English
The natural reindexing map given by a pair of equivalences e_m and e_n is a linear equivalence between CStarMatrix m n A and CStarMatrix l o A over R.
Русский
Естественное переиндексирование по парам эквиваленций e_m, e_n образует линейное эквивалентное отображение между CStarMatrix(m,n,A) и CStarMatrix(l,o,A) над R.
LaTeX
$$$C^*\text{-Matrix}_{m,n}(A) \cong_\text{linear}^R C^*\text{-Matrix}_{l,o}(A).$$$
Lean4
/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence. -/
def reindexₗ {l o : Type*} [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ l) (eₙ : n ≃ o) :
CStarMatrix m n A ≃ₗ[R] CStarMatrix l o A :=
{ Matrix.reindex eₘ eₙ with
map_add' M N := by ext; simp
map_smul' r M := by ext; simp }
