Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-07-28 21:09
663a7b8e
View on Github →
chore(InnerProductSpace/PiL2):
Fintype m
->
Finite m
(
#15232
)
Estimated changes
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
modified
theorem
Matrix.toEuclideanLin_eq_toLin
modified
theorem
Matrix.toEuclideanLin_eq_toLin_orthonormal