Theorems · Definition · group theory

AddLocalization.liftOn

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

Non-dependent recursion principle for AddLocalizations: given elements f a b : p for all a b, such that r S (a, b) (c, d) implies f a b = f c d, then f is defined on the whole Localization S.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoid