English
A variant providing a schema for proving properties of Laurent polynomials by reducing to monomials and sums, with a simpler recursor.
Русский
Вариант индукции для лаурентовских многочленов с упрощённой рекурсией.
LaTeX
$$$\\text{Induction_on}'(p, add, C_mul_T) : \\text{motive}(p)$$$
Lean4
/-- To prove something about Laurent polynomials, it suffices to show that
* the condition is closed under taking sums, and
* it holds for monomials.
-/
@[elab_as_elim]
protected theorem induction_on' {motive : R[T;T⁻¹] → Prop} (p : R[T;T⁻¹])
(add : ∀ p q, motive p → motive q → motive (p + q)) (C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)) : motive p :=
by
refine p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_ <;> try exact fun n f _ => C_mul_T _ f
convert C_mul_T 0 a
exact (mul_one _).symm
