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_iffView on Github →