English
The mem_range_of_degree_eq_one result: deg(minpoly_A(x)) = 1 implies x lies in the image of algebraMap A B.
Русский
Если deg(minpoly_A(x)) = 1, то x лежит в образе algebraMap A B.
LaTeX
$$$\\deg(\\minpoly_A(x)) = 1 \\Rightarrow x \\in (\\text{algebraMap}_{A\\to B}).\\mathrm{range}$$$
Lean4
/-- If a monic polynomial `p : A[X]` of degree `n` annihilates an element `x` in an `A`-algebra `B`,
such that `{xⁱ | 0 ≤ i < n} is linearly independent over `A`, then `p` is the minimal polynomial
of `x` over `A`. -/
theorem eq_of_linearIndependent {p : A[X]} (monic : p.Monic) (hp0 : p.aeval x = 0) (n : ℕ) (hpn : p.degree = n)
(ind : LinearIndependent A fun i : Fin n ↦ x ^ i.val) : minpoly A x = p :=
.symm <|
unique' _ _ monic hp0 fun q lt ↦
or_iff_not_imp_left.mpr fun ne hq ↦
ne <|
ext fun i ↦ by
rw [q.as_sum_range' _ ((natDegree_lt_iff_degree_lt ne).mpr (hpn ▸ lt))] at hq
obtain lt | le := lt_or_ge i n
·
simpa using
Fintype.linearIndependent_iff.mp ind (q.coeff ·)
(by simpa [Finset.sum_range, Algebra.smul_def] using hq) ⟨i, lt⟩
· exact coeff_eq_zero_of_degree_lt ((hpn ▸ lt).trans_le <| WithBot.coe_le_coe.mpr le)
