English
For x ∈ an algebra B over A, the minimal polynomial of x has degree one precisely when x lies in the image of the base algebra map from A to B.
Русский
Для элемента x ∈ B, минимальный полином над A имеет степень 1 тогда и только тогда, когда x лежит в образе отображения A → B.
LaTeX
$$$(\minpoly A x).degree = 1 \iff x \in (\operatorname{algebraMap} A B).range$$$
Lean4
theorem degree_eq_one_iff : (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range :=
by
refine ⟨minpoly.mem_range_of_degree_eq_one _ _, ?_⟩
rintro ⟨x, rfl⟩
haveI := Module.nontrivial A B
exact
(degree_X_sub_C x ▸ minpoly.min A (algebraMap A B x) (monic_X_sub_C x) (by simp)).antisymm
(Nat.WithBot.add_one_le_of_lt <| minpoly.degree_pos isIntegral_algebraMap)
