Theorems · Theorem · group theory

AddLocalization.ndrec_mk

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

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoid