Skip to content
Add "ready-to-merge" and "delegated" label from comment

[Merged by Bors] - feat: generalize LinearMap.exists_rightInverse_of_surjective to projective modules #60511

Sign in to view logs

[Merged by Bors] - feat: generalize LinearMap.exists_rightInverse_of_surjective to projective modules

[Merged by Bors] - feat: generalize LinearMap.exists_rightInverse_of_surjective to projective modules #60511

This job was skipped