Commit 2024-11-04 12:29 6376f401

View on Github →

chore(Data/Quot): rename surjective_*_mk => *.mk_surjective (#16410) surjective_quot_mk => Quot.mk_surjective surjective_quotient_mk => Quotient.mk_surjective surjective_quotient_mk' => Quotient.mk'_surjective Quotient.surjective_Quotient_mk'' => Quotient.mk''_surjective This is consistent with the naming of most lemmas about Function.Surjective in mathlib. Also make Setoid parameters implicit.

Estimated changes

added theorem Quot.mk_surjective
added theorem Quotient.mk_surjective
modified theorem Monoid.Coprod.mk_surjective
modified theorem t2Quotient.surjective_mk