nsmul_coe — Mathlib

English

Scaling in the nonnegative rationals corresponds to rational scaling after coercion: ↑(n • q) = n • (q : ℚ).

Русский

Умножение на n в ℚ≥0 соответствует масштабированию в ℚ после приведения: ↑(n • q) = n • (q : ℚ).

LaTeX

$$$$ \uparrow(n \;\!\cdot\; q) = n \;\!\cdot\; (q : \mathbb{Q}). $$$$

Lean4

@[norm_cast]
theorem nsmul_coe (q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • (q : ℚ) :=
  coeHom.toAddMonoidHom.map_nsmul _ _

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