Mathlib v3 is deprecated. Go to Mathlib v4

Theorem map_real_smul

Modification history

2022-10-31 09:21
src/topology/instances/real_vector_space.lean
chore(analysis/complex/basic): golf some proofs (#17259) …
Added map_real_smulView on Github →