English
The minimal polynomial of root f over K is related to f via a normalization by the leading coefficient.
Русский
Минполином корня f над K связан с f нормировкой по ведущему коэффициенту.
LaTeX
$$minpoly K (root f) = f * C f.leadingCoeff⁻¹ for f ≠ 0$$
Lean4
theorem minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C f.leadingCoeff⁻¹ :=
by
have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf
refine (minpoly.unique K _ f'_monic ?_ ?_).symm
· rw [map_mul, aeval_eq, mk_self, zero_mul]
intro q q_monic q_aeval
have commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f :=
by
ext
· simp only [RingHom.comp_apply, mk_C, lift_of]
rfl
· simp only [RingHom.comp_apply, mk_X, lift_root]
rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero, Nat.cast_le, natDegree_mul hf,
natDegree_C, add_zero]
· apply natDegree_le_of_dvd
· have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
exact mk_eq_zero.1 this
· exact q_monic.ne_zero
· rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
