ofReal_nnqsmul

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.ofReal_nnqsmul

English

For q ∈ ℚ and r ∈ ℝ, ofReal(q • r) = q • r.

Русский

Для q ∈ ℚ и r ∈ ℝ верно: ofReal(q • r) = q • r.

LaTeX

$$$$\operatorname{ofReal}(q \cdot r) = q \cdot r.$$$$

Lean4

@[simp, norm_cast]
theorem ofReal_nnqsmul (q : ℚ≥0) (r : ℝ) : ofReal (q • r) = q • r := by simp [NNRat.smul_def]

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

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

Разделы

Аффилиация

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