Theorems · Definition · group theory

ConGen.Rel.recOn

∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} {a a_1 : M}
  (t : ConGen.Rel r a a_1),
  (∀ (x y : M) (a : r x y), motive x y ⋯) →
    (∀ (x : M), motive x x ⋯) →
      (∀ {x y : M} (a : ConGen.Rel r x y), motive x y a → motive y x ⋯) →
        (∀ {x y z : M} (a : ConGen.Rel r x y) (a_2 : ConGen.Rel r y z), motive x y a → motive y z a_2 → motive x z ⋯) →
          (∀ {w x y z : M} (a : ConGen.Rel r w x) (a_2 : ConGen.Rel r y z),
              motive w x a → motive y z a_2 → motive (w * y) (x * z) ⋯) →
            motive a a_1 t

Defined in

Mathlib.GroupTheory.Congruence.Defs

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Mul