Pi.induction

Stream: Is there code for X?

[Christian Merten]

We have docs#Finsupp.induction, but I can't find

import Mathlib.Algebra.BigOperators.Pi

lemma Pi.induction {ι M : Type*} [Fintype ι] [DecidableEq ι] [AddCommMonoid M]
    (p : (ι → M) → Prop) (f : ι → M) (h0 : p 0) (hadd : ∀ f g, p f → p g → p (f + g))
    (hsingle : ∀ i m, p (Pi.single i m)) : p f := by
  rw [← Finset.univ_sum_single f]
  exact Finset.sum_induction _ _ hadd h0 (by simp [hsingle])

If it does not exist, do we want it? The proof is short, but this is handy for the induction tactic.

[Edward van de Meent]

at first glance, i'd say this is not a property of Pi, but rather of Fintype ι

[Edward van de Meent]

or, actually, this seems like a kind of closure induction?

[Edward van de Meent]

something along the lines of Basis, maybe

[Christian Merten]

Yes of course, this is related to docs#Submodule.span_induction, but this does not answer the question.

[Edward van de Meent]

if we want this, i think we might also want a mul-version?

[Edward van de Meent]

although i don't know if there is a mul version of Pi.single

[Christian Merten]

Edward van de Meent said:

although i don't know if there is a mul version of Pi.single

there is, its docs#Pi.mulSingle

[Christian Merten]

Edward van de Meent said:

if we want this, i think we might also want a mul-version?

and yes, this is the actual code:

@[to_additive]
lemma Pi.induction_mul {ι M : Type*} [Fintype ι] [DecidableEq ι] [CommMonoid M] (p : (ι → M) → Prop)
    (f : ι → M) (hone : p 1) (hmul : ∀ f g, p f → p g → p (f * g))
    (hsingle : ∀ i m, p (Pi.mulSingle i m)) : p f := by
  rw [← Finset.univ_prod_mulSingle f]
  exact Finset.prod_induction _ _ hmul hone (by simp [hsingle])

[Eric Wieser]

Things like docs#LinearMap.pi_ext seem related here