orthonormalBasisOneI_repr_apply

Mathlib.Analysis.InnerProductSpace.PiL2

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

English

For any z in C, its coordinates with respect to the basis {1,i} are (Re z, Im z).

Русский

Для любого z в C координаты по базису {1,i} равны (Re z, Im z).

LaTeX

$$$\mathrm{repr}(z) = (\mathrm{Re}(z), \mathrm{Im}(z))$$$

Lean4

@[simp]
theorem orthonormalBasisOneI_repr_apply (z : ℂ) : Complex.orthonormalBasisOneI.repr z = ![z.re, z.im] :=
  rfl

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

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

Разделы

Аффилиация

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