Theorems · Theorem · linear algebra

Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row

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

Multiplying by all the matrices either in listTransvecCol M and listTransvecRow M kills all the coefficients in the last column but the last one.

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field