real_smul

Mathlib.Data.Complex.Basic

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

English

For all real x, z ∈ ℂ, x • z = x z.

Русский

Для всех действительных x, z ∈ ℂ: x • z = x z.

LaTeX

$$$\\forall x \\in \\mathbb{R}, \\forall z \\in \\mathbb{C}, x \\cdot z = x z$$$

Lean4

@[simp]
theorem real_smul {x : ℝ} {z : ℂ} : x • z = x * z :=
  rfl

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

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

Разделы

Аффилиация

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