Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_R_or_C.real_smul_eq_coe_smul

Modification history

2022-08-09 09:08
src/data/complex/is_R_or_C.lean
feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879) …
Added is_R_or_C.real_smul_eq_coe_smulView on Github →