Theorems · Theorem · commutative algebra

IsLocalization.iff_map_piEvalRingHom

∀ {ι : Type u_1} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)] (S' : Type u_4) [inst_1 : CommSemiring S']
  [inst_2 : Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i)) [Finite ι],
  IsLocalization M S' ↔ IsLocalization (Submonoid.pi Set.univ fun i => Submonoid.map (Pi.evalRingHom R i) M) S'

Defined in

Mathlib.RingTheory.Localization.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraFinite