Def Complex.mulAux

Modification history

2026-04-13 14:38
Mathlib/Data/Complex/Basic.lean
perf(Data/Complex/Basic): don't expose complex multiplication (#37994) …
Added Complex.mulAuxView on Github →