Theorem ContinuousLinearMap.isQuotientMap_of_finiteDimensional

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.isQuotientMap_of_finiteDimensionalView on Github →