English
A weaker induction principle for mv-polynomials: closures under adding new monomials with nonzero coefficients, combined with existing induction hypotheses, suffice to prove a property for all mv-polynomials.
Русский
Слабеее принцип индукции для mv-многочленов: достаточны замыкания по добавлению новых мономов с ненулевыми коэффициентами и существующие гипотезы индукции.
LaTeX
$$$P(p) \text{ if } P(monomial a b) \land P(p) \to P(p) $ и т.д.$$
Lean4
/-- Similar to `MvPolynomial.induction_on` but only a weak form of `h_add` is required.
In particular, this version only requires us to show
that `motive` is closed under addition of nontrivial monomials not present in the support.
-/
@[elab_as_elim]
theorem monomial_add_induction_on {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ a, motive (C a))
(monomial_add :
∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((monomial a b) + f)) :
motive p :=
Finsupp.induction p (C_0.rec <| C 0) monomial_add
