English
The powerBasisAux' is a Basis for AdjoinRoot g, given a monic polynomial g and irreducible conditions.
Русский
PowerBasisAux' образует базис AdjoinRoot g при моничности g и ирредуциируемости.
LaTeX
$$powerBasisAux' hg is Basis$$
Lean4
/-- The power basis `1, root g, ..., root g ^ (d - 1)` for `AdjoinRoot g`,
where `g` is a monic polynomial of degree `d`. -/
@[simps]
def powerBasis' (hg : g.Monic) : PowerBasis R (AdjoinRoot g)
where
gen := root g
dim := g.natDegree
basis := powerBasisAux' hg
basis_eq_pow
i := by
simp only [powerBasisAux', Basis.coe_ofEquivFun, LinearEquiv.coe_symm_mk]
rw [Finset.sum_eq_single i]
· rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
· intro j _ hj
rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]
-- Fix `DecidableEq` mismatch
· intros
have := Finset.mem_univ i
contradiction
