fromEnd_apply — Mathlib

English

Let f be an endomorphism of M and w a function ι → R. Then the endomorphism PiToModule.fromEnd applied to w equals f applied to the R-linear combination of the base family b weighted by w; i.e., fromEnd R b f w = f(∑_i w_i b_i).

Русский

Пусть f — конечное отображение (конечномерного типа) M, и пусть w: ι → R. Тогда fromEnd R b f applied to w равно f(∑_i w_i b_i).

LaTeX

$$$\\mathrm{fromEnd}(R,b,f)(w) = f\\left(\\sum_{i} w_i\, b_i\\right)$$$

Lean4

theorem fromEnd_apply (f : Module.End R M) (w : ι → R) :
    PiToModule.fromEnd R b f w = f (Fintype.linearCombination R b w) :=
  rfl

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