Theorems · Theorem · linear algebra

Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction

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

Inductive step for the reduction: if one knows that any size r matrix can be reduced to diagonal form by elementary operations, then one deduces it for matrices over Fin r ⊕ Unit.

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field