Theorems · Definition · group theory
Localization
{M : Type u_1} → [inst : CommMonoid M] → Submonoid M → Type u_1The localization of a CommMonoid at one of its submonoids (as a quotient type).
- Cited by
- 270 results in Mathlib
- Foundations
- Depth 21 from the axioms, rests on 172 definitions · uses propext
- Assumes
- CommMonoid
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.
- Submonoidstatement and proof · cited by 3,086
- CommMonoidstatement and proof · cited by 2,264
- OreLocalizationproof · cited by 90
Cited by323
Results whose statement or proof uses this declaration.
- Localization.AtPrimeproof · cited by 299
- FractionRingproof · cited by 200
- Localization.Awayproof · cited by 162
- Localization.mkstatement · cited by 110
- HomogeneousLocalization.valstatement · cited by 51
- LocalizedModule.mapstatement and proof · cited by 29
- Localization.mk_eq_mk'statement · cited by 25
- HomogeneousLocalization.val_injectivestatement · cited by 24
- PrimeSpectrum.PiLocalizationproof · cited by 20
- Localization.monoidOfstatement · cited by 17
- Localization.AtPrime.map_eq_maximalIdealstatement and proof · cited by 17
- ModuleCat.localizedModulestatement and proof · cited by 16
Showing the 200 most cited of 323.