Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-16 10:37
5b262109
View on Github →
feat(Data/Matrix/Basis): small helper lemma for
of
(
#21935
)
Estimated changes
Modified
Mathlib/Data/Matrix/Basis.lean
added
theorem
Matrix.of_symm_stdBasisMatrix