finsuppLequivDFinsupp_symm_apply — Mathlib

English

The inverse of the linear equivalence finsuppLequivDFinsupp has the same underlying map as DFinsupp.toFinsupp; i.e., the symmetry carries back to the DFinsupp representation.

Русский

Обратная часть линейного изоморфа finsuppLequivDFinsupp имеет такое же основанное отображение, что и DFinsupp.toFinsupp; то есть симметричное отображение возвращает DFinsupp-образ.

LaTeX

$$$\\uparrow(\\text{LinearEquiv.symm}(\\text{finsuppLequivDFinsupp }(R))) = \\text{DFinsupp.toFinsupp}$$$

Lean4

@[simp]
theorem finsuppLequivDFinsupp_symm_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M] [∀ m : M, Decidable (m ≠ 0)]
    [Module R M] : ↑(LinearEquiv.symm (finsuppLequivDFinsupp (ι := ι) (M := M) R)) = DFinsupp.toFinsupp :=
  rfl

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