English
An alternative elimination principle for mv-polynomials: once you know how to handle constants and add-mendable monomials, you can conclude for arbitrary monomials.
Русский
Альтернативный принцип исключения для mv-многочленов: зная как обращаться с константами и мономами, допускающими добавление, можно заключить для любых мономов.
LaTeX
$$$P(p) \Leftarrow (\forall a, P(C a)) \land (\forall p,n, P(p) \to P(p * X_n)) \Rightarrow P(\text{monomial } p)$$$
Lean4
/-- Similar to `MvPolynomial.induction_on` but only a yet weaker form of `h_add` is required.
In particular, this version only requires us to show
that `motive` is closed under addition of monomials not present in the support
for which `motive` is already known to hold.
-/
theorem 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) → motive ((monomial a b) + f))
(mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) : motive p :=
monomial_add_induction_on p C fun a b f ha hb hf => monomial_add a b f ha hb hf <| induction_on_monomial C mul_X a b
