Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.of_real_smul

Modification history

2021-03-10 20:43
src/data/complex/basic.lean
feat(data/complex/module): transfer all `has_scalar ℝ` structures to `ℂ` (#6562) …
Deleted complex.of_real_smulView on Github →
2021-02-28 07:50
src/data/complex/basic.lean
chore(*): more line lengths (#6472)
Modified complex.of_real_smulView on Github →
2020-07-14 11:42
src/data/complex/basic.lean
feat(analysis/normed_space): complex Hahn-Banach theorem (#3286) …
Added complex.of_real_smulView on Github →