reindexₐ_apply — Mathlib

English

Identity for reindexₐ at entries: reindexₐ applied to M at i,j equals Matrix.reindex applied to M at i,j.

Русский

Тождество для reindexₐ на элементах: reindexₐ(M)_{i j} = (Matrix.reindex e e M)_{i j}.

LaTeX

$$$\mathrm{reindex}_{\mathsf{a}}(R,A,e)\,M\;i\;j = (\text{Matrix.reindex } e e\,M)\;i\;j$$$

Lean4

@[simp]
theorem reindexₐ_apply [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Star A] [Module R A] {e : m ≃ n}
    {M : CStarMatrix m m A} {i : n} {j : n} : reindexₐ R A e M i j = Matrix.reindex e e M i j :=
  rfl

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