Def LinearMap.restrictScalarsLinearMap

Modification history

2024-11-07 11:59
Mathlib/Algebra/Module/Algebra.lean
feat: define restrictions of perfect pairings (#18559) …
Deleted LinearMap.restrictScalarsLinearMapView on Github →
2023-02-19 14:29
Mathlib/Algebra/Module/Algebra.lean
feat: port Algebra.Module.Algebra (#2370)
Added LinearMap.restrictScalarsLinearMapView on Github →