Theorems · Theorem · linear algebra

Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow

∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod).IsTwoBlockDiagonal

Multiplying by all the matrices either in listTransvecCol M and listTransvecRow M turns the matrix in block-diagonal form.

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field