Theorems · Theorem · ring theory

OreLocalization.universalHom_unique

∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_3}
  [inst_2 : Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : OreLocalization S R →+* T),
  (∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) → φ = OreLocalization.universalHom f fS hf

Defined in

Mathlib.RingTheory.OreLocalization.Ring

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringOreLocalization.OreSetSemiring