Theorems · Theorem · general algebraic systems

DFinsupp.induction

∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i),
  p 0 → (∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p ((fun₀ | i => b) + f)) → p f

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClass