Theorems · Definition · group theory

Con.liftOnUnits

{M : Type u_1} →
  {α : Type u_4} →
    [inst : Monoid M] →
      {c : Con M} →
        c.Quotientˣ →
          (f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α) →
            (∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1)
                (hyx' : c (y' * x') 1), c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx') →
              α

In order to define a function (Con.Quotient c)ˣ → α on the units of Con.Quotient c, where c : Con M is a multiplicative congruence on a monoid, it suffices to define a function f that takes elements x y : M with proofs of c (x * y) 1 and c (y * x) 1, and returns an element of α provided that f x y _ _ = f x' y' _ _ whenever c x x' and c y y'.

Defined in

Mathlib.GroupTheory.Congruence.Defs

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Monoid