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