Theorem Complex.coe_smul

Modification history

2023-08-10 19:52

Mathlib/Data/Complex/Module.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Complex.coe_smul View on Github →

2023-05-02 07:59

Mathlib/Data/Complex/Module.lean

feat: port Data.Complex.Module (#3737)

Added Complex.coe_smul View on Github →