trunc_C — Mathlib

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

Похожие утверждения