Theorems · Theorem · linear algebra

Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm

∀ {R : Type u_1} {n : Type u_5} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (p : n → Prop)
  [inst_3 : 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),
  A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

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.

Defined in

Mathlib.Data.Matrix.ColumnRowPartitioned

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFintypeDecidableEqDecidablePred