Def ContinuousLinearMap.rangeRestrict

Modification history

2024-05-07 01:05

Mathlib/Topology/Algebra/Module/Basic.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted ContinuousLinearMap.rangeRestrict View on Github →

2024-01-17 20:26

Mathlib/Topology/Algebra/Module/Basic.lean

feat: injective continuous linear map with closed range is a continuous linear equivalence (#9756) …

Added ContinuousLinearMap.rangeRestrict View on Github →