Commit 2024-10-09 13:34 98905d23

View on Github →

feat: InnerProductSpace (SeparationQuotient E) (#17576)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem Inseparable.inner_eq_inner

added theorem SeparationQuotient.inner_mk_mk