trunc'_C — Mathlib

English

As before, truncation distributes over multiplication by a constant: trunc(C(a)·p) = C(a)·trunc(p).

Русский

Как и раньше, усечение распространяется на умножение константы: trunc(C(a)·p) = C(a)·trunc(p).

LaTeX

$$$$ \\operatorname{trunc} R n (C a \\cdot p) = C a \\cdot \\operatorname{trunc} R n p. $$$$

Lean4

@[simp]
theorem trunc'_C (n : σ →₀ ℕ) (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
    exfalso; apply H; subst m; exact zero_le n

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