Commit 2026-04-13 14:38 03ab9049

View on Github →

perf(Data/Complex/Basic): don't expose complex multiplication (#37994) This PR uses the module system to not expose the definition of complex multiplication.

Estimated changes

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

Modified Mathlib/Data/Complex/Basic.lean

added theorem Complex.mk_mul_mk

added def Complex.mulAux

modified theorem Complex.smul_im

modified theorem Complex.smul_re

Modified Mathlib/LinearAlgebra/Complex/Module.lean