Commit 2024-05-12 15:16 3f8be61e
View on Github →chore: change InnerProductSpace.complexToReal to a definition (#12840)
The instance docs#InnerProductSpace.complexToReal create some diamond with docs#PiLp.innerProductSpace, see Zulip.
This PR changes this instance to a def instead and add the instance
instance : InnerProductSpace ℝ ℂ := innerProductSpace.complexToReal