Theorems · Definition · group theory
Localization.monoidOf
{M : Type u_1} → [inst : CommMonoid M] → (S : Submonoid M) → S.LocalizationMap (Localization S)Natural homomorphism sending x : M, M a CommMonoid, to the equivalence class of
(x, 1) in the Localization of M at a Submonoid.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Quot.sound
- Assumes
- CommMonoid
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.
- MonoidHomproof · cited by 3,629
- Submonoidstatement and proof · cited by 3,086
- CommMonoidstatement and proof · cited by 2,264
- MonoidHom.compproof · cited by 469
- Localizationstatement · cited by 270
- Submonoid.LocalizationMapstatement · cited by 147
- Localization.mkproof · cited by 110
- Con.Quotientproof · cited by 48
- MonoidHom.inlproof · cited by 32
- Con.mk'proof · cited by 22
- Localization.rproof · cited by 16
Cited by23
Results whose statement or proof uses this declaration.
- Localization.mulEquivOfQuotientproof · cited by 7
- Localization.mk_eq_monoidOf_mk'statement · cited by 5
- Localization.mk_eq_monoidOf_mk'_applystatement and proof · cited by 4
- Algebra.GrothendieckGroup.liftproof · cited by 2
- Localization.mk_eq_mk'_applyproof · cited by 2
- Algebra.GrothendieckGroup.ofproof · cited by 2
- Localization.toLocalizationMap_eq_monoidOfstatement · cited by 1
- Localization.mk_one_eq_monoidOf_mkstatement · cited by 1
- Localization.mulEquivOfQuotient_mk'statement and proof · cited by 1
- Localization.mulEquivOfQuotient_symm_mk'statement and proof · cited by 1
- Localization.Away.monoidOfproof · cited by 1
- Algebra.GrothendieckGroup.lift_applystatement and proof · cited by 0