Theorems · Theorem · group theory

Monoid.CoprodI.induction_left

∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {motive : Monoid.CoprodI M → Prop}
  (m : Monoid.CoprodI M),
  motive 1 → (∀ {i : ι} (m : M i) (x : Monoid.CoprodI M), motive x → motive (Monoid.CoprodI.of m * x)) → motive m

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

1 results in Mathlib

Foundations

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

Assumes

Monoid