Commit 2025-11-14 19:40 fef46774

View on Github →

feat(Analysis/InnerProductSpace/Basic): add a simp lemma (#30793) Add a simp lemma (for benchmarking purposes - to see if it doesn't have a bad performance impact).

Estimated changes

Modified Mathlib/Analysis/Convex/Cone/InnerDual.lean

Modified Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem inner_self_eq_one_of_norm_one

modified theorem inner_self_im

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

Modified Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

Modified Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthonormal.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/InnerProductSpace/ProdL2.lean

Modified Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

Modified Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/Quaternion.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.im_ofReal_pow

added theorem RCLike.re_ofReal_pow

Modified Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

Modified Mathlib/Geometry/Euclidean/Triangle.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/Topology/VectorBundle/Riemannian.lean