Theorems · Definition · group theory

AddLocalization.rec

{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)) →
          (∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) →
            (x : AddLocalization S) → p x

Dependent recursion principle for AddLocalizations: given elements f a b : p (mk a b) for all a b, such that r S (a, b) (c, d) implies f a b = f c d (with the correct coercions), then f is defined on the whole AddLocalization S.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoid