domLCongr_refl — Mathlib

English

The identity equivalence on a index set α induces the identity linear equivalence on the finitely supported functions α →₀ M.

Русский

Тождественное отображение на множество индексов α порождает тождественное линейное эквивалентное отображение на множества функций с конечной опорой α →₀ M.

LaTeX

$$$\\mathrm{domLCongr}(\\mathrm{Equiv.refl}\\,\\alpha) = \\mathrm{LinearEquiv.refl}\,R\\,(\\alpha \\to_0 M)$$$

Lean4

@[simp]
theorem domLCongr_refl : Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M) :=
  LinearEquiv.ext fun _ => equivMapDomain_refl _

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