trunc_add — Mathlib

English

Truncation commutes with addition: trunc n (φ + ψ) = trunc n φ + trunc n ψ.

Русский

Уточнение-сложение: усечение n от (φ + ψ) равно усечению n от φ плюс усечение n от ψ.

LaTeX

$$$\\operatorname{trunc} n (\\phi + \\psi) = \\operatorname{trunc} n \\phi + \\operatorname{trunc} n \\psi$$$

Lean4

@[simp]
theorem trunc_add (n) (φ ψ : R⟦X⟧) : trunc n (φ + ψ) = trunc n φ + trunc n ψ :=
  Polynomial.ext fun m => by
    simp only [coeff_trunc, Polynomial.coeff_add]
    split_ifs with H
    · rfl
    · rw [zero_add]

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