Theorems · Theorem · group theory

DirectSum.induction_on

∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  {motive : (DirectSum ι fun i => β i) → Prop} (x : DirectSum ι fun i => β i),
  motive 0 →
    (∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)) →
      (∀ (x y : DirectSum ι fun i => β i), motive x → motive y → motive (x + y)) → motive x

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEq