powerBasisAux'_repr_symm_apply — Mathlib

English

The representation map of powerBasisAux' is given by evaluation against coefficients: it sends a coefficient function c to the corresponding combination of monomials in mk g.

Русский

Карта представления powerBasisAux' соответствует коэффициентам: она отправляет функцию коэффициентов c в соответствующее сочетание мономов в mk g.

LaTeX

$$powerBasisAux'.repr.symm c = mk g (sum over i of monomial i (c i))$$

Lean4

theorem powerBasisAux'_repr_symm_apply (hg : g.Monic) (c : Fin g.natDegree →₀ R) :
    (powerBasisAux' hg).repr.symm c = mk g (∑ i : Fin _, monomial i (c i)) :=
  rfl

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