Commit 2024-05-06 15:57 1b80fd08

View on Github →

feat(Data/Quot): add surjective_quotient_mk (#12702) add missing surjective_quotient_mk to mirror surjective_quotient_mk', Quotient.surjective_quotient_mk'', and surjective_quot_mk.

Estimated changes

added theorem surjective_quotient_mk