powerBasisAux'_repr_apply_to_fun — Mathlib

English

For monic g, and c a finitely supported function from Fin g.natDegree to R, the symm-repr evaluation equals the mk g of the sum of monomials with coefficients c.

Русский

Для моничного g и c: Fin g.natDegree →₀ R, выполняется равенство repr.symm c = mk g (∑ i, monomial i (c i)).

LaTeX

$$powerBasisAux' hg repr.symm c = mk g (Σ i monomial i (c i))$$

Lean4

@[simp]
theorem powerBasisAux'_repr_apply_to_fun (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) :
    (powerBasisAux' hg).repr f i = (modByMonicHom hg f).coeff ↑i :=
  rfl

Похожие утверждения