English
The construction powerBasisAux builds a basis for AdjoinRoot f; its properties relate to minpoly_root and linear independence of powers of root.
Русский
Конструкция powerBasisAux строит базис AdjoinRoot f; ее свойства связаны с minpoly_root и линейной независимостью степеней корня.
LaTeX
$$powerBasisAux hf is a Basis for AdjoinRoot f with generators 1, root f, ..., root f^{d-1}$$
Lean4
/-- The elements `1, root f, ..., root f ^ (d - 1)` form a basis for `AdjoinRoot f`,
where `f` is an irreducible polynomial over a field of degree `d`. -/
def powerBasisAux (hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f) :=
by
let f' := f * C f.leadingCoeff⁻¹
have deg_f' : f'.natDegree = f.natDegree :=
by
rw [natDegree_mul hf, natDegree_C, add_zero]
· rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
· rw [← deg_f', ← minpoly_eq]
exact linearIndependent_pow (root f)
· rintro y -
rw [← deg_f', ← minpoly_eq]
apply (isIntegral_root hf).mem_span_pow
obtain ⟨g⟩ := y
use g
rw [aeval_eq]
rfl
