Theorems · Theorem · linear algebra

Matrix.fromCols_mul_fromRows_eq_one_comm

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

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".

Defined in

Mathlib.Data.Matrix.ColumnRowPartitioned

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFintypeFintypeFintypeDecidableEqDecidableEqDecidableEq