truncateFun_add — Mathlib

English

truncateFun n preserves addition: truncateFun n (x + y) = truncateFun n x + truncateFun n y.

Русский

Усечение сохраняет сложение: truncateFun n (x + y) = truncateFun n x + truncateFun n y.

LaTeX

$$$ \operatorname{truncateFun}(n)(x + y) = \operatorname{truncateFun}(n)(x) + \operatorname{truncateFun}(n)(y) $$$

Lean4

@[simp]
theorem truncateFun_add (x y : 𝕎 R) : truncateFun n (x + y) = truncateFun n x + truncateFun n y := by
  witt_truncateFun_tac

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