English
Analog of polynomial induction: a motive on mv-polynomials is established by induction over finsupp decomposition using monomials and addition.
Русский
Аналог полиномиальной индукции: мотив для mv-многочленов устанавливается по индукции над разложением на мономы через сложение.
LaTeX
$$$P(p) \Leftarrow \bigl(P(monomial(u,a)) \; \text{для всех } u,a\bigr)\Rightarrow P(p)$$$
Lean4
/-- Analog of `Polynomial.induction_on'`.
To prove something about mv_polynomials,
it suffices to show the condition is closed under taking sums,
and it holds for monomials. -/
@[elab_as_elim]
theorem induction_on' {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R)
(monomial : ∀ (u : σ →₀ ℕ) (a : R), P (monomial u a)) (add : ∀ p q : MvPolynomial σ R, P p → P q → P (p + q)) :
P p :=
Finsupp.induction p
(suffices P (MvPolynomial.monomial 0 0) by rwa [monomial_zero] at this
show P (MvPolynomial.monomial 0 0) from monomial 0 0)
fun _ _ _ _ha _hb hPf => add _ _ (monomial _ _) hPf
