ofReal_mul'

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.ofReal_mul'

English

Scalar multiplication distributes: ↑r * z = ⟨r z.re, r z.im⟩.

Русский

Скалярное умножение распределяется: ↑r * z = ⟨r z.re, r z.im⟩.

LaTeX

$$↑r * z = { re := r*z.re, im := r*z.im }$$

Lean4

theorem ofReal_mul' (r : ℝ) (z : ℂ) : ↑r * z = ⟨r * z.re, r * z.im⟩ :=
  ext (re_ofReal_mul _ _) (im_ofReal_mul _ _)

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

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

Разделы

Аффилиация

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