reindexRange_apply — Mathlib

English

Let b be a basis of a module M over a semiring R. Then the reindexing map restricted to the image of b is the identity: for every x in range(b), b.reindexRange(x) = x.

Русский

Пусть b — базис модуля M над полем-кольцом R. Тогда отображение переиндексации, ограниченное на образе b, является тождественным: для каждого x ∈ range(b) выполняется b.reindexRange(x) = x.

LaTeX

$$$\\forall x \\in \\mathrm{range}(b),\\; b\\!\\cdot\\mathrm{reindexRange}\\, x = x.$$$

Lean4

@[simp]
theorem reindexRange_apply (x : range b) : b.reindexRange x = x :=
  by
  rcases x with ⟨bi, ⟨i, rfl⟩⟩
  exact b.reindexRange_self i

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