Mathlib Map

Theorems · Definition · group theory

AddCon.toSetoid

{M : Type u_1} → [inst : Add M] → AddCon M → Setoid M

The equivalence relation underlying an additive congruence relation.

Defined in
Mathlib.GroupTheory.Congruence.Defs
Cited by
20 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Add
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddCon.Quotient · cited by 54AddCon.QuotientAddCon.comap · cited by 14AddCon.comapAddCon.refl · cited by 6AddCon.reflPresentedAddMonoid.mk · cited by 5PresentedAddMonoid.mkAddCon.symm · cited by 4AddCon.symmAddCon.add' · cited by 3AddCon.add'AddCon.toSetoid_injective · cited by 3AddCon.toSetoid_injectiveAddCon.toSetoid_inj · cited by 2AddCon.toSetoid_injAddCon.trans · cited by 2AddCon.transAddCon.congr · cited by 2AddCon.congrAddCon.addConGen_eq · cited by 1AddCon.addConGen_eqModuleCon.mk.inj · cited by 1mk.injModuleCon.mk.noConfusion · cited by 1mk.noConfusionAddCon.toSetoid_bot · cited by 1AddCon.toSetoid_botAddCon.toSetoid_top · cited by 1AddCon.toSetoid_topAddCon · cited by 138AddConAddCon.toSetoidCITED BYCITES

Cites1

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

  • AddConstatement and proof · cited by 138

Cited by33

Results whose statement or proof uses this declaration.