Theorems · Theorem · commutative algebra

IsLocalization.Away.mk

∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R),
  IsUnit ((algebraMap R S) r) →
    (∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a) →
      (∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b) → IsLocalization.Away r S

Specialized constructor for IsLocalization.Away.

Defined in

Mathlib.RingTheory.Localization.Away.Basic

Cited by

3 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebra