Theorems · Theorem · commutative algebra

IsLocalization.isLocalization_of_is_exists_mul_mem

∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (M N : Submonoid R) [IsLocalization M S], M ≤ N → (∀ (x : ↥N), ∃ m, m * ↑x ∈ M) → IsLocalization N S

If M ≤ N are submonoids of R such that ∀ x : N, ∃ m : R, m * x ∈ M, then the localization at N is equal to the localization of M.

Defined in

Mathlib.RingTheory.Localization.LocalizationLocalization

Cited by

2 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIsLocalization