measurableEquivRealProd_apply

Mathlib.MeasureTheory.Measure.Lebesgue.Complex

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

English

The measurableEquivRealProd applied to a complex number a yields the pair (a.re, a.im).

Русский

Применение measurableEquivRealProd к комплексному числу a даёт пару (a().re, a().im).

LaTeX

$$$\text{measurableEquivRealProd}(a) = (a^{\mathrm{re}}, a^{\mathrm{im}})$$$

Lean4

@[simp]
theorem measurableEquivRealProd_apply (a : ℂ) : measurableEquivRealProd a = (a.re, a.im) :=
  rfl

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

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

Разделы

Аффилиация

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