Commit 2024-10-19 00:06 992ec73d

View on Github →

feat: generalize LinearMap.exists_rightInverse_of_surjective to projective modules (#17560) Previously it only held in vector spaces.

Estimated changes

Modified Mathlib/Algebra/Module/Projective.lean

added theorem LinearMap.exists_rightInverse_of_surjective

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

deleted theorem LinearMap.exists_rightInverse_of_surjective

Modified Mathlib/LinearAlgebra/Dimension/LinearMap.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/Topology/Algebra/SeparationQuotient.lean