map_equiv — Mathlib

English

The equivalence b.equiv b (id) is the identity linear equivalence on M.

Русский

Эквивалентность на идентичности является тождественным линейным отображением.

LaTeX

$$$b.\\mathrm{equiv}\, b\, (\\mathrm{id}_{ι}) = \\mathrm{LinearEquiv.Refl}\\, R\\ M.$$$

Lean4

@[simp]
theorem map_equiv (b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') : b.map (b.equiv b' e) = b'.reindex e.symm :=
  by
  ext i
  simp

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