English
An induction principle for mv-polynomials: to prove a property for all monomials, it suffices to verify it for the constant monomial and show closure under multiplication by X_n.
Русский
Принцип индукции для mv-многочленов: чтобы доказать свойство для всех мономов, достаточно проверить для константного монома и показать замкнутость относительно умножения на X_n.
LaTeX
$$$\forall s,a,\; P(monomial(s,a)) \,\text{ если }\; (\forall a, P(C a)) \land (\forall p,n, P(p) \to P(p X_n))$$$
Lean4
@[elab_as_elim]
theorem induction_on_monomial {motive : MvPolynomial σ R → Prop} (C : ∀ a, motive (C a))
(mul_X : ∀ p n, motive p → motive (p * X n)) : ∀ s a, motive (monomial s a) :=
by
intro s a
apply @Finsupp.induction σ ℕ _ _ s
· change motive (monomial 0 a)
exact C a
· intro n e p _hpn _he ih
have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
intro e
induction e with
| zero => simp [ih]
| succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
simp [add_comm, monomial_add_single, this]
