coe_nsmul

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_nsmul

English

For r ∈ ℝ≥0 and n ∈ ℕ, the real-valued coercion of n • r equals n • (r : ℝ).

Русский

Для r ∈ ℝ≥0 и n ∈ ℕ, преобразование в Real от n • r равно n • (r : ℝ).

LaTeX

$$$\uparrow(n \cdot r) = n \cdot (r : \mathbb{R})$$$

Lean4

@[simp, norm_cast]
theorem coe_nsmul (r : ℝ≥0) (n : ℕ) : ↑(n • r) = n • (r : ℝ) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru