Commit 2023-04-05 08:46 0c99e2f5

View on Github →

feat: port Topology.Instances.RealVectorSpace (#3270)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/RealVectorSpace.lean

added def AddEquiv.toRealLinearEquiv

added theorem AddMonoidHom.coe_toRealLinearMap

added def AddMonoidHom.toRealLinearMap

added theorem map_real_smul