coe_toCircle

Mathlib.Analysis.SpecialFunctions.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Real.Angle.coe_toCircle

English

The complex coordinate of the point θ.toCircle is cos θ + i sin θ.

Русский

Комплексная координата точки θ.toCircle равна cos θ + i sin θ.

LaTeX

$$$$ (\theta^{\text{toCircle}})_{\mathbb{C}} = \cos \theta + i \sin \theta. $$$$

Lean4

theorem coe_toCircle (θ : Angle) : (θ.toCircle : ℂ) = θ.cos + θ.sin * I :=
  by
  induction θ using Real.Angle.induction_on
  simp [exp_mul_I]

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

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

Разделы

Аффилиация

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