Theorems · Theorem · linear algebra

Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec

∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  ∃ L L',
    ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
        (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal

There exist two lists of TransvectionStruct such that multiplying by them on the left and on the right makes a matrix block-diagonal.

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field