Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-30 08:52
39b61a6a
View on Github →
chore(Data/Matrix): some trivial lemmas about
row
and
col
(
#17243
)
Estimated changes
Modified
Mathlib/Data/Matrix/RowCol.lean
added
theorem
Matrix.mulVec_col_eq_const
added
theorem
Matrix.row_mulVec_eq_const
added
theorem
Matrix.row_mul_col