English
If the base algebra map A → B is injective, then the minimal polynomial of a ∈ A mapped to B is X − C a.
Русский
Если отображение A → B инъективно, то минимальный полином образа элемента a ∈ A в B равен X − C a.
LaTeX
$$$\minpoly A (\operatorname{algebraMap} A B a) = X - C a$$$
Lean4
/-- If `B/A` is an injective ring extension, and `a` is an element of `A`,
then the minimal polynomial of `algebraMap A B a` is `X - C a`. -/
theorem eq_X_sub_C_of_algebraMap_inj (a : A) (hf : Function.Injective (algebraMap A B)) :
minpoly A (algebraMap A B a) = X - C a := by
nontriviality A
refine (unique' A _ (monic_X_sub_C a) ?_ ?_).symm
· rw [map_sub, aeval_C, aeval_X, sub_self]
simp_rw [or_iff_not_imp_left]
intro q hl h0
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl
rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢
rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
