Mathlib Map

Theorems · Theorem · logic and foundations

Quotient.mk_surjective

∀ {α : Sort u_1} {s : Setoid α}, Function.Surjective (Quotient.mk s)

Quotient.mk is a surjective function.

Defined in
Mathlib.Data.Quot
Cited by
16 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Module.free_of_flat_of_isLocalRing · cited by 7Module.free_of_flat_of_is…CochainComplex.HomComplex.CohomologyClass.mk_surjective · cited by 7CohomologyClass.mk_surjec…ArchimedeanClass.mk_surjective · cited by 3ArchimedeanClass.mk_surje…DividedPowerAlgebra.mkAlgHom_surjective · cited by 2DividedPowerAlgebra.mkAlg…Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing · cited by 2Polynomial.quotient_mk_co…Asymptotics.IsBigO.multisetProd · cited by 2IsBigO.multisetProdSymmetricAlgebra.algHom_surjective · cited by 1SymmetricAlgebra.algHom_s…MulArchimedeanClass.mk_surjective · cited by 1MulArchimedeanClass.mk_su…Asymptotics.IsEquivalent.multisetProd · cited by 1IsEquivalent.multisetProdT2Quotient.surjective_mk · cited by 1T2Quotient.surjective_mkAsymptotics.IsLittleO.multisetProd · cited by 1IsLittleO.multisetProdMatrix.ProjGenLinGroup.mk_surjective · cited by 0ProjGenLinGroup.mk_surjec…Cardinal.mk_abelianization_le · cited by 0Cardinal.mk_abelianizatio…DoubleQuot.ker_quotLeftToQuotSup · cited by 0DoubleQuot.ker_quotLeftTo…IsLocalization.Away.quotient_of_isIdempotentElem · cited by 0Away.quotient_of_isIdempo…Quot.mk_surjective · cited by 34Quot.mk_surjectiveQuotient.mk_surjectiveCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by16

Results whose statement or proof uses this declaration.