Theorems · Theorem · group theory

Monoid.PushoutI.induction_on

∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  {φ : (i : ι) → H →* G i} {motive : Monoid.PushoutI φ → Prop} (x : Monoid.PushoutI φ),
  (∀ (i : ι) (g : G i), motive ((Monoid.PushoutI.of i) g)) →
    (∀ (h : H), motive ((Monoid.PushoutI.base φ) h)) →
      (∀ (x y : Monoid.PushoutI φ), motive x → motive y → motive (x * y)) → motive x

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidMonoid