Def InnerProductSpace.complexToReal

Modification history

2024-08-07 01:32

Mathlib/Analysis/InnerProductSpace/Basic.lean

feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace (#14024) …

Modified InnerProductSpace.complexToReal View on Github →

2024-05-12 15:16

Mathlib/Analysis/InnerProductSpace/Basic.lean

chore: change `InnerProductSpace.complexToReal` to a definition (#12840) …

Added InnerProductSpace.complexToReal View on Github →