Def AddMonoidHom.toRealLinearMap

Modification history

2023-04-05 08:46

Mathlib/Topology/Instances/RealVectorSpace.lean

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

Added AddMonoidHom.toRealLinearMap View on Github →