Commit 2026-04-28 22:05 27fd4b00

View on Github →

feat: a continuous linear map to a finite dimensional space is strict (#38474) Needed for #38471

Estimated changes

Modified Mathlib/Analysis/Normed/Module/Complemented.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

added theorem ContinuousLinearMap.exists_rightInverse_of_surjective

deleted theorem ContinuousLinearMap.exists_right_inverse_of_surjective

added theorem ContinuousLinearMap.isQuotientMap_of_finiteDimensional

added theorem ContinuousLinearMap.isStrictMap_of_finiteDimensional

modified theorem LinearMap.isClosedEmbedding_of_injective