Theorems · Theorem · group theory

Finsupp.induction

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

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

12 results in Mathlib

Foundations

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

Assumes

AddZeroClass