mathlib

06c7a487 - Fix: `complex.coe_smul` should be protected