linearEquiv_refl — Mathlib

English

If each i-th component uses the identity linear equivalence, the resulting mapRange linear equivalence is the identity on the whole DFinsupp space.

Русский

Если для каждой компоненты i применить тождественное линейное эквалентное отображение, то полученное отображение mapRange.linea rEquiv является тождественным на всем пространстве DFinsupp.

LaTeX

$$$\\mathrm{mapRange.linearEquiv}\\; (\\lambda i, \\mathrm{LinearEquiv.refl}\\; R\\; (\\beta_1 i)) = \\mathrm{LinearEquiv.refl}\\; R\\; (\\mathrm{DFinsupp}\\; (\\beta_1))$$$

Lean4

@[simp]
theorem linearEquiv_refl : (mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl _ _ :=
  LinearEquiv.ext mapRange_id

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