Theorems · Definition · group theory

AddConGen.Rel.below.casesOn

∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop}
  {motive_1 : {a a_1 : M} → (t : AddConGen.Rel r a a_1) → AddConGen.Rel.below t → Prop} {a a_1 : M}
  {t : AddConGen.Rel r a a_1} (t_1 : AddConGen.Rel.below t),
  (∀ (x y : M) (a : r x y), motive_1 ⋯ ⋯) →
    (∀ (x : M), motive_1 ⋯ ⋯) →
      (∀ {x y : M} (a : AddConGen.Rel r x y) (ih : AddConGen.Rel.below a) (a_ih : motive x y a), motive_1 ⋯ ⋯) →
        (∀ {x y z : M} (a : AddConGen.Rel r x y) (a_2 : AddConGen.Rel r y z) (ih : AddConGen.Rel.below a)
            (a_ih : motive x y a) (ih_1 : AddConGen.Rel.below a_2) (a_ih_1 : motive y z a_2), motive_1 ⋯ ⋯) →
          (∀ {w x y z : M} (a : AddConGen.Rel r w x) (a_2 : AddConGen.Rel r y z) (ih : AddConGen.Rel.below a)
              (a_ih : motive w x a) (ih_1 : AddConGen.Rel.below a_2) (a_ih_1 : motive y z a_2), motive_1 ⋯ ⋯) →
            motive_1 t t_1

Defined in

Mathlib.GroupTheory.Congruence.Defs

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

Add