trunc'_C_mul — Mathlib

English

The truncated product with a constant on the left equals the product of the constant and the truncated product.

Русский

Усечение умножения слева константой равно произведению константы на усечённый результат.

LaTeX

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

Lean4

@[simp]
theorem trunc'_C_mul (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) :
    trunc' R n (C a * p) = MvPolynomial.C a * trunc' R n p := by ext m; simp [coeff_trunc']

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