Commit 2024-07-18 09:55 36e3f75c

View on Github →

chore(Matrix/Transvection): add length/get lemmas (#14777)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

added theorem Matrix.Pivot.length_listTransvecCol

added theorem Matrix.Pivot.length_listTransvecRow

added theorem Matrix.Pivot.listTransvecCol_get

added theorem Matrix.Pivot.listTransvecRow_get