Theorems · Definition · group theory
AddLocalization
{M : Type u_1} → [inst : AddCommMonoid M] → AddSubmonoid M → Type u_1The localization of an AddCommMonoid at one of its submonoids (as a quotient type).
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- AddSubmonoidstatement and proof · cited by 1,178
- AddOreLocalizationproof · cited by 44
Cited by50
Results whose statement or proof uses this declaration.
- AddLocalization.mkstatement · cited by 28
- AddLocalization.addMonoidOfstatement · cited by 13
- AddLocalization.addEquivOfQuotientstatement · cited by 7
- AddLocalization.mk_eq_mk_iffstatement · cited by 5
- AddLocalization.mkHomstatement · cited by 3
- AddLocalization.mk_addstatement · cited by 3
- AddLocalization.mk_eq_addMonoidOf_mk'statement · cited by 3
- AddLocalization.mk_eq_addMonoidOf_mk'_applystatement and proof · cited by 3
- Algebra.GrothendieckAddGroupproof · cited by 3
- AddLocalization.induction_onstatement and proof · cited by 2
- AddLocalization.liftOnstatement and proof · cited by 2
- AddLocalization.liftOn₂statement and proof · cited by 2