Mathlib Map

Theorems · Definition · group theory

Localization.Away

{M : Type u_1} → [CommMonoid M] → M → Type u_1

Given x : M, the Localization of M at the Submonoid generated by x, as a quotient.

Defined in
Mathlib.GroupTheory.MonoidLocalization.Away
Cited by
162 results in Mathlib
Foundations
Depth 25 from the axioms, rests on 340 definitions · uses propext, Classical.choice, Quot.sound
Assumes
CommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Localization.awayMap · cited by 33Localization.awayMapRingHom.Locally · cited by 28RingHom.LocallyHomogeneousLocalization.awayMap · cited by 27HomogeneousLocalization.a…AlgebraicGeometry.IsAffineOpen.basicOpen · cited by 19IsAffineOpen.basicOpenRingHom.OfLocalizationSpan · cited by 16RingHom.OfLocalizationSpanRingHom.OfLocalizationSpanTarget · cited by 14RingHom.OfLocalizationSpa…Localization.awayMapₐ · cited by 8Localization.awayMapₐAlgebraicGeometry.Proj.toBasicOpenOfGlobalSections · cited by 7Proj.toBasicOpenOfGlobalS…AlgebraicGeometry.basicOpenIsoSpecAway · cited by 7AlgebraicGeometry.basicOp…RingHom.OfLocalizationSpanTarget.ofLocalizationSpan · cited by 7OfLocalizationSpanTarget.…Polynomial.UniversalCoprimeFactorizationRing · cited by 7Polynomial.UniversalCopri…IsLocalization.Away.finitePresentation · cited by 7Away.finitePresentationLocalization.awayLift · cited by 5Localization.awayLiftAlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop · cited by 5Scheme.affineOpenCoverOfS…Algebra.Generators.compLocalizationAwayAlgHom · cited by 5Generators.compLocalizati…CommMonoid · cited by 2264CommMonoidSubmonoid.powers · cited by 408Submonoid.powersLocalization · cited by 270LocalizationLocalization.AwayCITED BYCITES

Cites3

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

Cited by195

Results whose statement or proof uses this declaration.