Theorems · Theorem · group theory

AddLocalization.liftOn_mk

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

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoid