Theorems · Definition · group theory
AddLocalization.addMonoidOf
{M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → S.LocalizationMap (AddLocalization S)Natural homomorphism sending x : M, M an AddCommMonoid, to the equivalence class of
(x, 0) in the Localization of M at a Submonoid.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- AddMonoidHomproof · cited by 3,230
- AddSubmonoidstatement and proof · cited by 1,178
- AddMonoidHom.compproof · cited by 339
- AddSubmonoid.LocalizationMapstatement · cited by 119
- AddCon.Quotientproof · cited by 54
- AddLocalizationstatement · cited by 38
- AddMonoidHom.inlproof · cited by 29
- AddLocalization.mkproof · cited by 28
- AddCon.mk'proof · cited by 21
- AddLocalization.rproof · cited by 14
Cited by18
Results whose statement or proof uses this declaration.
- AddLocalization.addEquivOfQuotientproof · cited by 7
- AddLocalization.mk_eq_addMonoidOf_mk'_applystatement and proof · cited by 3
- AddLocalization.mk_eq_addMonoidOf_mk'statement · cited by 3
- Algebra.GrothendieckAddGroup.liftproof · cited by 2
- Algebra.GrothendieckAddGroup.ofproof · cited by 2
- AffineAddMonoid.embeddingproof · cited by 1
- AddLocalization.mk_zero_eq_addMonoidOf_mkstatement · cited by 1
- AddLocalization.addEquivOfQuotient_mk'statement and proof · cited by 1
- AddLocalization.addEquivOfQuotient_symm_mk'statement and proof · cited by 1
- AddLocalization.Away.addMonoidOfproof · cited by 1
- AffineAddMonoid.embedding_injectiveproof · cited by 0
- Algebra.GrothendieckAddGroup.lift_applystatement and proof · cited by 0