Commit 2026-04-17 05:47 2ca3076f

View on Github →

perf(Data/Complex/Basic): no_expose the Inv and Norm instance (#38007) This PR hides some more implementation details of complex numbers. It would be possible to no_expose even more definitions, but this could be at the cost of some proof writing convenience.

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/Complex/Norm.lean

modified theorem Complex.norm_def

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

modified def UpperHalfPlane.I

modified theorem UpperHalfPlane.I_im

modified theorem UpperHalfPlane.I_re

Modified Mathlib/Data/Complex/Basic.lean