truncateFun_nsmul — Mathlib

English

truncateFun n preserves natural-scalar multiplication: truncateFun n (m • x) = m • truncateFun n x.

Русский

Усечение сохраняет умножение на натуральный скаляр: truncateFun n (m • x) = m • truncateFun n x.

LaTeX

$$$ \operatorname{truncateFun}(n)(m \cdot x) = m \cdot \operatorname{truncateFun}(n)(x) $$$

Lean4

theorem truncateFun_nsmul (m : ℕ) (x : 𝕎 R) : truncateFun n (m • x) = m • truncateFun n x := by witt_truncateFun_tac

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