hasNatScalar — Mathlib

English

There is a natural-number scalar action on TruncatedWittVector defined by m • x = truncateFun(n)(m • x.out).

Русский

Существует скалярное действие натуральных чисел на TruncatedWittVector: m • x = truncateFun(n)(m • x.out).

LaTeX

$$$ m \cdot x = \mathrm{truncateFun}(n)(m \cdot x.\mathrm{out}) $$$

Lean4

instance hasNatScalar : SMul ℕ (TruncatedWittVector p n R) :=
  ⟨fun m x => truncateFun n (m • x.out)⟩

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