Theorems · Theorem · linear algebra

Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux

∀ {𝕜 : Type u_3} [inst : Field 𝕜] (n : Type) [inst_1 : Fintype n] [inst_2 : DecidableEq n] (M : Matrix n n 𝕜),
  ∃ L L' D,
    (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod =
      Matrix.diagonal D

Any matrix can be reduced to diagonal form by elementary operations. Formulated here on Type 0 because we will make an induction using Fin r. See exists_list_transvec_mul_mul_list_transvec_eq_diagonal for the general version (which follows from this one and reindexing).

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFintypeDecidableEq