Theorem Orthonormal.of_isEmpty

Modification history

2025-05-29 19:36
Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
feat: lemmas about `Orthonormal` and `Fin` (#25205) …
Added Orthonormal.of_isEmptyView on Github →