English
Specializing to the partition n = n1 ⊔ n2 via a predicate p, with A1 on {i: p i} and A2 on {i: ¬p i}, and B1, B2 on the corresponding parts, the same inverse-commutation holds: fromCols A1 A2 · fromRows B1 B2 = 1 iff fromRows B1 B2 · fromCols A1 A2 = 1.
Русский
Уточнение к разделению множества n на подмножества по предикату p: A1 на {i | p i}, A2 на {i | ¬p i}, 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
/-- The lemma `fromCols_mul_fromRows_eq_one_comm` specialized to the case where the index sets
`n₁` and `n₂`, are the result of subtyping by a predicate and its complement. -/
theorem equiv_compl_fromCols_mul_fromRows_eq_one_comm [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p]
(A₁ : Matrix n { i // p i } R) (A₂ : Matrix n { i // ¬p i } R) (B₁ : Matrix { i // p i } n R)
(B₂ : Matrix { i // ¬p i } n R) : fromCols A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromCols A₁ A₂ = 1 :=
fromCols_mul_fromRows_eq_one_comm (Equiv.sumCompl p).symm A₁ A₂ B₁ B₂
