English
There is an induction principle for Laurent polynomials built by successive multiplications by T^(-n). If a property holds for all polynomials f and natural n via the map toLaurent f multiplied by T^(-n), then the property holds for every Laurent polynomial.
Русский
Существует принцип индукции для лоурентовых многочленов, построенных последовательными умножениями на T^(-n). Если свойство верно для всех f и натуральных n через отображение toLaurent f умноженное на T^(-n), то свойство верно для любого лаурентового многочлена.
LaTeX
$$$\forall f : R[T;T^{-1}],\ motive : (\forall (f : R[X]) (n : \mathbb{N}),\ motive( toLaurent f * T (-n))) → \motive f$$$
Lean4
/-- This is a version of `exists_T_pow` stated as an induction principle. -/
@[elab_as_elim]
theorem induction_on_mul_T {motive : R[T;T⁻¹] → Prop} (f : R[T;T⁻¹])
(mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-n))) : motive f :=
by
rcases f.exists_T_pow with ⟨n, f', hf⟩
rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub, ← mul_assoc, ← hf]
exact mul_T ..
