Theorems · Definition · commutative algebra

Algebra.Generators.localizationAway

{R : Type u} →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (r : R) → [IsLocalization.Away r S] → Algebra.Generators R S Unit

If S is the localization of R away from r, we obtain a canonical generator mapping to the inverse of r.

Defined in

Mathlib.RingTheory.Extension.Generators

Cited by

23 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsLocalization.Away