Theorem SeparationQuotient.inner_mk_mk

Modification history

2024-12-20 05:04

Mathlib/Analysis/InnerProductSpace/Basic.lean

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

Modified SeparationQuotient.inner_mk_mk View on Github →

2024-10-09 13:34

Mathlib/Analysis/InnerProductSpace/Basic.lean

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

Added SeparationQuotient.inner_mk_mk View on Github →