Theorems · Theorem · group theory

Finsupp.induction_linear

∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M),
  motive 0 →
    (∀ (f g : ι →₀ M), motive f → motive g → motive (f + g)) → (∀ (a : ι) (b : M), motive fun₀ | a => b) → motive f

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

16 results in Mathlib

Foundations

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

Assumes

AddZeroClass