reindexLinearEquiv — Mathlib

English

Reindexing a matrix's rows and columns by equivalences yields a linear equivalence between the corresponding matrix spaces.

Русский

Переиндексация строк и столбцов матрицы по эквиваленциям задаёт линейное эквивалентное отображение между соответствующими пространствами матриц.

LaTeX

$$$ \mathrm{reindexLinearEquiv}\ R\ A\ e_m\ e_n : \mathrm{Matrix}\ m n A \cong_\!{\!R} \mathrm{Matrix}\ m' n' A. $$$

Lean4

/-- The natural map that reindexes a matrix's rows and columns with equivalent types,
`Matrix.reindex`, is a linear equivalence. -/
def reindexLinearEquiv (eₘ : m ≃ m') (eₙ : n ≃ n') : Matrix m n A ≃ₗ[R] Matrix m' n' A :=
  { reindex eₘ eₙ with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

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