Theorems · Theorem · group theory

Finsupp.induction_on_max

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

A finitely supported function can be built by adding up single a b for increasing a. The lemma induction_on_max₂ swaps the argument order in the sum.

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddZeroClassLinearOrder