English
To prove a property for Laurent polynomials, it suffices to show it is closed under addition and holds for monomials, and is preserved under left multiplication by constants and by monomials T n and T(-n).
Русский
Чтобы доказать свойство для лаурентовских многочленов, достаточно показать, что оно замкнуто относительно сложения и выполняется для мономов, а также сохраняется при левом умножении на константы и мономы T n и T(-n).
LaTeX
$$$\\text{InductionOn} \\ M(p) := (\\forall a, M(C a)) \\land (\\forall p,q, M p \\land M q \\Rightarrow M(p+q)) \\\\ \\land (\\forall n,a, M(C a * T n) \\Rightarrow M(C a * T(n+1))) \\\\ \\land (\\forall n,a, M(C a * T(-n)) \\Rightarrow M(C a * T(-n-1))) \\Rightarrow M(p)$$$
Lean4
@[simp]
theorem _root_.Polynomial.toLaurent_C (r : R) : toLaurent (Polynomial.C r) = C r :=
by
convert Polynomial.toLaurent_C_mul_T 0 r
simp only [Int.ofNat_zero, T_zero, mul_one]
