Theorems · Definition · linear algebra
Matrix.Pivot.listTransvecRow
{𝕜 : Type u_3} →
[Field 𝕜] → {r : ℕ} → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 → List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)A list of transvections such that multiplying on the right with these transvections will replace the last row with zeroes.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- Matrixstatement and proof · cited by 4,303
- Matrix.transvectionproof · cited by 24
Cited by9
Results whose statement or proof uses this declaration.
- Matrix.Pivot.mul_listTransvecRow_last_col_takestatement and proof · cited by 2
- Matrix.Pivot.length_listTransvecRowstatement · cited by 1
- Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_colstatement and proof · cited by 1
- Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_rowstatement and proof · cited by 1
- Matrix.Pivot.mul_listTransvecRow_last_colstatement and proof · cited by 1
- Matrix.Pivot.mul_listTransvecRow_last_rowstatement and proof · cited by 1
- Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zeroproof · cited by 1
- Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRowstatement · cited by 1
- Matrix.Pivot.listTransvecRow_getElemstatement and proof · cited by 0