English
Every Laurent polynomial f ∈ R[T;T^{-1}] can be written as toLaurent f' = f · T^n for some n ∈ ℕ and some f' ∈ R[X].
Русский
Каждый лоурентовый многочлен f ∈ R[T;T^{-1}] можно записать в виде toLaurent f' = f · T^n для некоторого n ∈ ℕ и некоторого f' ∈ R[X].
LaTeX
$$$\exists n \in \mathbb{N}\,\exists f' \in R[X],\ toLaurent f' = f \cdot T^{n}$$$
Lean4
theorem exists_T_pow (f : R[T;T⁻¹]) : ∃ (n : ℕ) (f' : R[X]), toLaurent f' = f * T n :=
by
refine f.induction_on' ?_ fun n a => ?_ <;> clear f
· rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow, mul_T_assoc,
Int.natCast_add]
· rcases n with n | n
· exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
· refine ⟨n + 1, Polynomial.C a, ?_⟩
simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.natCast_succ, mul_T_assoc, neg_add_cancel, T_zero, mul_one]
