English
Suppose the column-partitioned matrix fromCols A1 A2 and the row-partitioned matrix fromRows B1 B2 form a square matrix under a suitable equivalence. Then the equation fromCols A1 A2 · fromRows B1 B2 = 1 holds if and only if the reverse order fromRows B1 B2 · fromCols A1 A2 = 1.
Русский
Пусть блочная матрица fromCols A1 A2 и блочная матрица fromRows B1 B2 образуют квадратную матрицу; тогда fromCols A1 A2 · fromRows B1 B2 = 1 тогда и только тогда, когда fromRows B1 B2 · fromCols A1 A2 = 1.
LaTeX
$$$ fromCols A_1 A_2 \cdot fromRows B_1 B_2 = 1 \;\Longleftrightarrow\; fromRows B_1 B_2 \cdot fromCols A_1 A_2 = 1 $$$
Lean4
/-- Multiplication of a matrix by its inverse is commutative.
This is the column and row partitioned matrix form of `Matrix.mul_eq_one_comm`.
The condition `e : n ≃ n₁ ⊕ n₂` states that `fromCols A₁ A₂` and `fromRows B₁ B₂` are "square".
-/
theorem fromCols_mul_fromRows_eq_one_comm [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁]
[DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R)
(B₂ : Matrix n₂ n R) : fromCols A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromCols A₁ A₂ = 1 :=
mul_eq_one_comm_of_equiv e
