Commit 2025-05-29 19:36 f3b26dd4

View on Github →

feat: lemmas about Orthonormal and Fin (#25205) This makes it easier to work with Orthonormal 𝕜 ![a, b, c]

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthonormal.lean

added theorem Orthonormal.of_isEmpty

added theorem orthonormal_vecCons_iff

Modified Mathlib/Logic/Pairwise.lean

added theorem pairwise_fin_succ_iff

added theorem pairwise_fin_succ_iff_of_isSymm