English
If p ∈ A[X] is irreducible and monic and p(x) = 0, then p = minpoly_A x.
Русский
Если p ∈ A[X] ирредуцируем и монический и p(x) = 0, тогда p = minpoly_A x.
LaTeX
$$Irreducible p ∧ p.Monic ∧ Polynomial.aeval x p = 0 ⇒ p = minpoly A x$$
Lean4
theorem eq_of_irreducible [Nontrivial B] {p : A[X]} (hp1 : Irreducible p) (hp2 : Polynomial.aeval x p = 0) :
p * C p.leadingCoeff⁻¹ = minpoly A x :=
by
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
apply eq_of_irreducible_of_monic
·
exact
Associated.irreducible
⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff, by rwa [← C_mul, inv_mul_cancel₀, C_1], by
rwa [← C_mul, mul_inv_cancel₀, C_1]⟩,
rfl⟩
hp1
· rw [aeval_mul, hp2, zero_mul]
· rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]
