nsmul_coe — Mathlib

English

Natural-number scalar multiplication intertwines with the embedding: n•⟨x, hx⟩ maps to n•x.

Русский

Умножение на натуральное число согласовано с внедрением: n•⟨x, hx⟩ отображается в n•x.

LaTeX

$$$ ↑(n \cdot r) = n \cdot (r : \alpha) $$$

Lean4

@[norm_cast]
theorem nsmul_coe (n : ℕ) (r : { x : α // 0 ≤ x }) : ↑(n • r) = n • (r : α) :=
  Nonneg.coeAddMonoidHom.map_nsmul _ _

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