Theorems · Definition · commutative algebra
Localization.algEquiv
{R : Type u_1} →
[inst : CommSemiring R] →
(M : Submonoid R) →
(S : Type u_2) →
[inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Localization M ≃ₐ[R] SThe localization of R at M as a quotient type is isomorphic to any other localization.
- Defined in
- Mathlib.RingTheory.Localization.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Submonoidstatement and proof · cited by 3,086
- AlgEquivstatement · cited by 1,681
- IsLocalizationstatement and proof · cited by 636
- Localizationstatement and proof · cited by 270
- IsLocalization.algEquivproof · cited by 45
Cited by17
Results whose statement or proof uses this declaration.
- FractionRing.algEquivproof · cited by 9
- Localization.tensorLeftAlgEquivproof · cited by 3
- Algebra.IsSmoothAt.exists_notMem_isStandardSmoothproof · cited by 2
- IsLocalization.lift_cardinalMkproof · cited by 2
- Localization.coe_algEquiv_symmstatement · cited by 1
- RingHom.OfLocalizationSpan.ofIsLocalizationproof · cited by 1
- RingHom.OfLocalizationSpanTarget.ofIsLocalizationproof · cited by 1
- Localization.algEquiv_mk'statement · cited by 1
- Localization.algEquiv_symm_applystatement and proof · cited by 1
- Localization.algEquiv_symm_mk'statement · cited by 1
- IsLocalization.lift_cardinalMk_leproof · cited by 1
- IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdxproof · cited by 1