Documentation

Project.ForMathlib.LocalizationAway

instance Localization.awayProd_isLocalization_closure' {R : Type u_1} [CommRing R] {t : Set R} (fin : t.Finite) :
IsLocalization (Submonoid.closure t) (Localization.Away (∏ ifin.toFinset, i))
noncomputable def Localization.closureFiniteEquiv {R : Type u_1} [CommRing R] {t : Set R} (fin : t.Finite) :
Localization (Submonoid.closure t) ≃ₐ[R] Localization.Away (∏ ifin.toFinset, i)
Equations
Instances For
    @[simp]
    theorem Localization.clousreFinite_comp {R : Type u_1} [CommRing R] {t : Set R} (fin : t.Finite) :
    @[simp]
    theorem Localization.closureFininite_symm_comp {R : Type u_1} [CommRing R] {t : Set R} (fin : t.Finite) :
    (↑(Localization.closureFiniteEquiv fin).symm).comp (Algebra.ofId R (Localization.Away (∏ ifin.toFinset, i))) = Algebra.ofId R (Localization (Submonoid.closure t))