Theorem AddMonoidHom.coe_toRealLinearMap

Modification history

2023-04-05 08:46
Mathlib/Topology/Instances/RealVectorSpace.lean
feat: port Topology.Instances.RealVectorSpace (#3270)
Added AddMonoidHom.coe_toRealLinearMapView on Github →