English
For all n ∈ ℤ and r ∈ R, trunc (C r * T^n) equals monomial(n.toNat) r if n ≥ 0, and equals 0 otherwise.
Русский
Для всех n ∈ ℤ и r ∈ R, усечение trunc(C r · T^n) равно мономиону n.toNat \, r, если n ≥ 0, иначе 0.
LaTeX
$$$\forall n \in \mathbb{Z}, \forall r \in R:\ \operatorname{trunc}(C(r) \cdot T^{n}) = \begin{cases} \operatorname{monomial}(n^{\mathrm{toNat}})\, r, & 0 \le n, \\ 0, & \text{иначе}. \end{cases}$$$
Lean4
@[simp]
theorem trunc_C_mul_T (n : ℤ) (r : R) : trunc (C r * T n) = ite (0 ≤ n) (monomial n.toNat r) 0 :=
by
apply (toFinsuppIso R).injective
simp only [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply, RingHom.toAddMonoidHom_eq_coe,
RingEquiv.toRingHom_eq_coe, Int.ofNat_eq_coe, AddMonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.apply_symm_apply,
toFinsuppIso_apply]
-- We need `erw` to see through the identification of `Finsupp` with `LaurentSeries`.
erw [comapDomain.addMonoidHom_apply Int.ofNat_injective]
split_ifs with n0
· rw [toFinsupp_monomial]
lift n to ℕ using n0
apply comapDomain_single
· rw [toFinsupp_inj]
ext a
have : a ≠ n := by omega
simp only [coeff_ofFinsupp, comapDomain_apply, Int.ofNat_eq_coe, coeff_zero, single_eq_of_ne this]
