Mathlib Changelog
v4
Changelog
About
Github
Theorem
orthonormal_vecCons_iff
Modification history
2025-05-29 19:36
Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
feat: lemmas about `Orthonormal` and `Fin` (#25205) …
Added
orthonormal_vecCons_iff
View on Github →