coeFnLinearMap_apply — Mathlib

English

The natural embedding of a DFinsupp into a pi-type is a linear map.

Русский

Естественное вложение DFinsupp в произведение по координатам является линейным отображением.

LaTeX

$$$$ \\mathrm{coeFnLinearMap}: (\\\\Pi_ i β_i) \\to_{\\\\ell} (\\\\ prod_i β_i) $$$$

Lean4

@[simp]
theorem coeFnLinearMap_apply [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (v : Π₀ i, β i) :
    coeFnLinearMap γ v = v :=
  rfl

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