Theorems · Theorem · group theory

Localization.liftOn_mk

∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S),
  (Localization.mk a b).liftOn f H = f a b

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommMonoid