finsuppLequivDFinsupp_apply_apply

English

The underlying function of the finsuppLequivDFinsupp equivalence, when viewed as a function from (ι →₀ M) to the dependent FinSupp, coincides with the standard Finsupp.toDFinsupp embedding.

Русский

Фундаментальная функция эквивалентности между (ι →₀ M) и DFinsupp совпадает с обычной вложенной отображением Finsupp.toDFinsupp.

LaTeX

$$$\\uparrow(\\text{finsuppLequivDFinsupp } (R)) = \\text{Finsupp.toDFinsupp}$$$

Lean4

@[simp]
theorem finsuppLequivDFinsupp_apply_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M] [∀ m : M, Decidable (m ≠ 0)]
    [Module R M] : (↑(finsuppLequivDFinsupp (M := M) R) : (ι →₀ M) → _) = Finsupp.toDFinsupp :=
  rfl

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