Theorems · Theorem · commutative algebra

IsLocalization.sec_spec

∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
  z * (algebraMap R S) ↑(IsLocalization.sec M z).2 = (algebraMap R S) (IsLocalization.sec M z).1

Given z : S, IsLocalization.sec M z is defined to be a pair (x, y) : R × M such that z * f y = f x (so this lemma is true by definition).

Defined in

Mathlib.RingTheory.Localization.Defs

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses Classical.choice

Assumes

CommSemiringCommSemiringAlgebraIsLocalization