Theorem Complex.mk_mul_mk

Modification history

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