English
Let K be a field, S a K-algebra, and x ∈ S integral over K. Then the family {x^i : i ∈ Fin((minpoly K x).natDegree)} is linearly independent over K.
Русский
Пусть K — поле, S — K-алгебра и x ∈ S интегрирован над K. Тогда семейство {x^i : i ∈ Fin((minpoly K x).natDegree)} линейно независимо над K.
LaTeX
$$$ \operatorname{LinearIndependent}_K \big( x^i \big)_{i : \mathrm{Fin}((\minpoly K x).natDegree)} $$$
Lean4
/-- Useful lemma to show `x` generates a power basis:
the powers of `x` less than the degree of `x`'s minimal polynomial are linearly independent. -/
theorem linearIndependent_pow [Algebra K S] (x : S) :
LinearIndependent K fun i : Fin (minpoly K x).natDegree => x ^ (i : ℕ) :=
by
by_cases h : IsIntegral K x; swap
· rw [minpoly.eq_zero h, natDegree_zero]
exact linearIndependent_empty_type
refine Fintype.linearIndependent_iff.2 fun g hg i => ?_
simp only at hg
simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg
apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_gt).mtr
· simp_rw [← C_mul_X_pow_eq_monomial]
exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _
· apply_fun lcoeff K i at h0
simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0
exact (if_pos <| Finset.mem_univ _).symm.trans h0
