coe_pos_real_smul

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.coe_pos_real_smul

English

The underlying complex of the action x • z equals the real scalar x times z in ℂ.

Русский

Узкое представление действия x • z равно x · z в ℂ.

LaTeX

$$↑(x • z) = (x : ℝ) • (z : ℂ)$$

Lean4

@[simp]
theorem coe_pos_real_smul : ↑(x • z) = (x : ℝ) • (z : ℂ) :=
  rfl

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

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

Разделы

Аффилиация

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