equiv — Mathlib

English

The repr of reindexed basis on its own vector is a singleton at that vector.

Русский

Представление перенормированного базиса на собственном векторе является синглетоном, соответствующим этому вектору.

LaTeX

$$$b.\\mathrm{reindexFinsetRange.repr}(b i) = \\mathrm{Finsupp.single}⟨b i, \\, \\mathrm{memImageOfMem}(b,\\mathrm{memUniv}(i))⟩\\, 1.$$$

Lean4

/-- If `b` is a basis for `M` and `b'` a basis for `M'`, and the index types are equivalent,
`b.equiv b' e` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `b' (e i)`. -/
protected def equiv : M ≃ₗ[R] M' :=
  b.repr.trans (b'.reindex e.symm).repr.symm

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