ofReal_zsmul

Mathlib.Data.Complex.Basic

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

English

Let n be an integer and r a real number. Then the complex number obtained by embedding n•r into ℂ equals n times the embedding of r into ℂ.

Русский

Пусть n ∈ ℤ и r ∈ ℝ. Тогда число в ℂ, полученное из n•r, равно n⋅(r в ℂ).

LaTeX

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

Lean4

@[norm_cast]
theorem ofReal_zsmul (n : ℤ) (r : ℝ) : ↑(n • r) = n • (r : ℂ) := by simp

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

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

Разделы

Аффилиация

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