Theorem Inseparable.inner_eq_inner

Modification history

2024-12-20 05:04

Mathlib/Analysis/InnerProductSpace/Basic.lean

chore(Analysis/InnerProductSpace): split large file (#20046) …

Modified Inseparable.inner_eq_inner View on Github →

2024-10-09 13:34

Mathlib/Analysis/InnerProductSpace/Basic.lean

feat: `InnerProductSpace (SeparationQuotient E)` (#17576)

Added Inseparable.inner_eq_inner View on Github →