Theorem ContinuousLinearMap.exists_rightInverse_of_surjective

Modification history

2026-04-28 22:05
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
feat: a continuous linear map to a finite dimensional space is strict (#38474) …
Added ContinuousLinearMap.exists_rightInverse_of_surjectiveView on Github →