reindexₗ_apply — Mathlib

English

Applying the reindexₗ equivalence to a matrix M at entry i,j gives the same value as applying Matrix.reindex to M at i,j.

Русский

Применение линейного эквивалента переиндексации к матрице M в позиции (i,j) даёт такое же значение, как и применение Matrix.reindex к M в (i,j).

LaTeX

$$$\text{reindex}_\ell(R,A,e_m,e_n)\,M\;i\;j = (\text{Matrix.reindex } e_m e_n\,M)\,i\,j$$$

Lean4

@[simp]
theorem reindexₗ_apply {l o : Type*} [Semiring R] [AddCommMonoid A] [Module R A] {eₘ : m ≃ l} {eₙ : n ≃ o}
    {M : CStarMatrix m n A} {i : l} {j : o} : reindexₗ R A eₘ eₙ M i j = Matrix.reindex eₘ eₙ M i j :=
  rfl

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