English
For any nonzero bound n, the truncation of a constant multivariate polynomial C(a) equals the same constant polynomial C(a).
Русский
При любом ненулевом ограничении n усечение константного многочлена C(a) совпадает с тем же константным многочленом.
LaTeX
$$$$ \\operatorname{trunc} R n (C a) = C a, \\quad \\text{when } n \\neq 0. $$$$
Lean4
@[simp]
theorem trunc_C (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : trunc R n (C a) = MvPolynomial.C a :=
MvPolynomial.ext _ _ fun m ↦ by
classical
rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C]
split_ifs with H <;>
first
| rfl
| try simp_all only [ne_eq, not_true_eq_false]
exfalso; apply H; subst m; exact Ne.bot_lt hnn