English
If a property P of polynomials is closed under sums and holds for all monomials, then P holds for every polynomial.
Русский
Если свойство P многочленов замкнуто относительно сумм и выполняется для всех мономов, то P выполняется для любого многочлена.
LaTeX
$$$\\forall p:\\,R[X],\\Big(\\forall p\\ q, P(p) \\land P(q) \\Rightarrow P(p+q)\\Big) \\land \\Big(\\forall n:\\,\\mathbb{N}, \\forall a:\\,R, P(monomial\\ n\\ a)\\Big) \\Rightarrow P(p).$$
Lean4
/-- To prove something about polynomials,
it suffices to show the condition is closed under taking sums,
and it holds for monomials.
-/
@[elab_as_elim]
protected theorem induction_on' {motive : R[X] → Prop} (p : R[X]) (add : ∀ p q, motive p → motive q → motive (p + q))
(monomial : ∀ (n : ℕ) (a : R), motive (monomial n a)) : motive p :=
Polynomial.induction_on p (monomial 0) add fun n a _h => by rw [C_mul_X_pow_eq_monomial]; exact monomial _ _
