toFunBilinear_apply_eq_smul — Mathlib

English

The toFunBilinear construction agrees with summing monomials: the bilinear map evaluated on sum(s) equals the sum of monomials weighted by the products a and r.

Русский

Конструкция toFunBilinear согласуется с суммами мономов: значение билинейного отображения на сумму равняется сумме мономов, взвешенных произведениями a и r.

LaTeX

$$$$ toFunBilinear\\, R\\, A\\, a\\, p = p.sum (\\lambda n r,\\ monomial\\ n\\ (a \\cdot algebraMap\\ R A\\ r)) $$$$

Lean4

@[simp]
theorem toFunBilinear_apply_eq_smul (a : A) (p : R[X]) : toFunBilinear R A a p = a • p.map (algebraMap R A) :=
  rfl

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