reindexRange — Mathlib

English

Given a basis b, one can form a new basis indexed by range b, called reindexRange, using the injective mapping from b.

Русский

Дан базис b, можно получить новый базис, индексированный по range b, названный reindexRange, с помощью инъекции из b.

LaTeX

$$$$ reindexRange : Basis\, (range\, b)\, R\, M $$$$

Lean4

/-- `b.reindexRange` is a basis indexed by `range b`, the basis vectors themselves. -/
def reindexRange : Basis (range b) R M :=
  haveI := Classical.dec (Nontrivial R)
  if h : Nontrivial R then b.reindex (Equiv.ofInjective b (Basis.injective b))
  else
    letI : Subsingleton R := not_nontrivial_iff_subsingleton.mp h
    .ofRepr (Module.subsingletonEquiv R M (range b))

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