Theorem map_real_smul

Modification history

2024-02-05 18:00
Mathlib/Topology/Instances/RealVectorSpace.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified map_real_smulView on Github →
2023-04-05 08:46
Mathlib/Topology/Instances/RealVectorSpace.lean
feat: port Topology.Instances.RealVectorSpace (#3270)
Added map_real_smulView on Github →