Theorem Matrix.Pivot.length_listTransvecCol

Modification history

2024-07-18 09:55
Mathlib/LinearAlgebra/Matrix/Transvection.lean
chore(Matrix/Transvection): add `length`/`get` lemmas (#14777)
Added Matrix.Pivot.length_listTransvecColView on Github →