ofReal_qsmul

Mathlib.Data.Complex.Basic

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

English

For q ∈ ℚ and r ∈ ℝ, the embedding commutes with rational scalar multiplication: 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_qsmul (q : ℚ) (r : ℝ) : ofReal (q • r) = q • r := by simp [Rat.smul_def]

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

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

Разделы

Аффилиация

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