Commit 2025-06-23 13:09 9cc0d159
View on Github →feat: lemmas about orthonormal bases (#26276) Write the inner product of two elements of an orthonormal basis as an if-then-else. Write the formula for the square norm in a real inner product space with an orthonormal basis to drop the norm around the inner product.