English
For any n ∈ ℤ and a ∈ R with a ≠ 0, deg(C a · T^n) equals some n (i.e., it is attached to the exponent n).
Русский
Для любого n ∈ ℤ и a ∈ R, если a ≠ 0, степень C a · T^n равна некоторому n (то есть соответствует степени экспоненты n).
LaTeX
$$$\forall {R} (n : \mathbb Z) (a : R), a \neq 0 \Rightarrow\ degree(C(a) \cdot T^{n}) = n$$$
Lean4
/-- The support of a polynomial `f` is a finset in `ℕ`. The lemma `toLaurent_support f`
shows that the support of `f.toLaurent` is the same finset, but viewed in `ℤ` under the natural
inclusion `ℕ ↪ ℤ`. -/
theorem toLaurent_support (f : R[X]) : f.toLaurent.support = f.support.map Nat.castEmbedding :=
by
generalize hd : f.support = s
revert f
refine Finset.induction_on s ?_ ?_ <;> clear s
· intro f hf
rw [Finset.map_empty, Finsupp.support_eq_empty, toLaurent_eq_zero]
exact Polynomial.support_eq_empty.mp hf
· intro a s as hf f fs
have : (erase a f).toLaurent.support = s.map Nat.castEmbedding :=
by
refine hf (f.erase a) ?_
simp only [fs, Finset.erase_eq_of_notMem as, Polynomial.support_erase, Finset.erase_insert_eq_erase]
rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T, support_add_eq,
Finset.insert_eq]
· congr
exact support_C_mul_T_of_ne_zero (Polynomial.mem_support_iff.mp (by simp [fs])) _
· rw [this]
exact Disjoint.mono_left (support_C_mul_T _ _) (by simpa)
