Def AddEquiv.toRealLinearEquiv

Modification history

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