truncateFun_mul — Mathlib

English

truncateFun n preserves multiplication: 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_mul (x y : 𝕎 R) : truncateFun n (x * y) = truncateFun n x * truncateFun n y := by
  witt_truncateFun_tac

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