English
Let Q be a property of Laurent polynomials. If Q holds for all toLaurent f with f ∈ R[X], and Q(f · T) implies Q(f) for all f, then Q holds for every Laurent polynomial.
Русский
Пусть Q — свойство лоурентовых многочленов. Если Q верно для всех toLaurent f, где f ∈ R[X], и если из Q(f · T) следует Q(f) для всех f, то Q верно для любого лаурентового многочлена.
LaTeX
$$$\forall f \in R[T;T^{-1}],\ Q(f) \\text{given conditions } Q( toLaurent f) \, and \, (\forall f, Q(f \cdot T) \Rightarrow Q(f)) \Rightarrow Q(f)$$$
Lean4
/-- Suppose that `Q` is a statement about Laurent polynomials such that
* `Q` is true on *ordinary* polynomials;
* `Q (f * T)` implies `Q f`;
it follow that `Q` is true on all Laurent polynomials. -/
theorem reduce_to_polynomial_of_mul_T (f : R[T;T⁻¹]) {Q : R[T;T⁻¹] → Prop} (Qf : ∀ f : R[X], Q (toLaurent f))
(QT : ∀ f, Q (f * T 1) → Q f) : Q f :=
by
induction f using LaurentPolynomial.induction_on_mul_T with
| _ f n
induction n with
| zero => simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
| succ n hn => convert QT _ _; simpa using hn
