Theorems · Theorem · ring theory

OreLocalization.universalMulHom_commutes

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

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidOreLocalization.OreSetMonoid