English
Reindexing a matrix M by an equivalence e : m ≃ n preserves block triangular structure: (reindex e e M) is BlockTriangular with respect to b exactly when M is BlockTriangular with respect to b ∘ e.
Русский
Перекодировка матрицы M по эквиваленции e : m ≃ n сохраняет блочную треугольность: (reindex e e M) блочно-треугольна относительно b тогда и только тогда, когда M блочно-треугольна относительно b ∘ e.
LaTeX
$$$(\mathrm{reindex}\ e\ e\ M)\; \BlockTriangular\; b \iff M\;\BlockTriangular\; (b \circ e)$$$
Lean4
theorem blockTriangular_reindex_iff {b : n → α} {e : m ≃ n} :
(reindex e e M).BlockTriangular b ↔ M.BlockTriangular (b ∘ e) :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· convert h.submatrix
simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]
· convert h.submatrix
simp only [comp_assoc b e e.symm, Equiv.self_comp_symm, comp_id]
