Theorem Matrix.smul_mat_cons

Modification history

2025-11-07 15:55
Mathlib/LinearAlgebra/Matrix/Notation.lean
chore(Data): deprecate `toReal_eq_toReal`, `count_eq_of_nodup` and `smul_mat_cons` (#28484)
Deleted Matrix.smul_mat_consView on Github →
2023-04-20 04:08
Mathlib/Data/Matrix/Notation.lean
feat: port Data.Matrix.Notation (#3427) …
Added Matrix.smul_mat_consView on Github →