English
If f is monic of degree d, the elements 1, root f, ..., root f^{d-1} form a basis for AdjoinRoot f over the base field.
Русский
Если f моничeскf степени d, то 1, root f, ..., root f^{d-1} образуют базис AdjoinRoot f над базовым полем.
LaTeX
$$powerBasis f Monic$$
Lean4
/-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `AdjoinRoot g`,
where `g` is a monic polynomial of degree `d`. -/
def powerBasisAux' (hg : g.Monic) : Basis (Fin g.natDegree) R (AdjoinRoot g) :=
.ofEquivFun
{ toFun := fun f i => (modByMonicHom hg f).coeff i
invFun := fun c => mk g <| ∑ i : Fin g.natDegree, monomial i (c i)
map_add' := fun f₁ f₂ => funext fun i => by simp only [(modByMonicHom hg).map_add, coeff_add, Pi.add_apply]
map_smul' := fun f₁ f₂ =>
funext fun i => by simp only [(modByMonicHom hg).map_smul, coeff_smul, Pi.smul_apply, RingHom.id_apply]
left_inv
f :=
AdjoinRoot.induction_on _ f fun f =>
Eq.symm <|
mk_eq_mk.mpr <| by
simp only [modByMonicHom_mk, sum_modByMonic_coeff hg degree_le_natDegree]
rw [modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel]
exact dvd_mul_right _ _
right_inv := fun x =>
funext fun i => by
nontriviality R
simp only [modByMonicHom_mk]
rw [(modByMonic_eq_self_iff hg).mpr, finset_sum_coeff]
· simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
· simp_rw [← C_mul_X_pow_eq_monomial]
exact (degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _ }
-- This lemma could be autogenerated by `@[simps]` but unfortunately that would require
-- unfolding that causes a timeout.
-- This lemma should have the simp tag but this causes a lint issue.
