toFunAlgHom_apply_tmul — Mathlib

English

A refined coefficient-wise equality expressing the same antidiagonal sum in the expanded form of the product of polynomials.

Русский

Уточнённое равенство коэффициентов, выражающее ту же сумму по антидиагонали в развернутой форме произведения полиномов.

LaTeX

$$$\\text{(same antidiagonal sum equality as Aux)}$$$

Lean4

theorem toFunAlgHom_apply_tmul (a : A) (p : R[X]) :
    toFunAlgHom R A (a ⊗ₜ[R] p) = p.sum fun n r => monomial n (a * (algebraMap R A) r) :=
  toFunBilinear_apply_eq_sum R A _ _

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