sin_conj

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

For any z, sin(conj z) = conj(sin z).

Русский

Для любого z верно: sin(зеркальное сопряжение z) = сопряжённое к sin z.

LaTeX

$$$ \sin(\overline{z}) = \overline{\sin z}. $$$

Lean4

theorem sin_conj : sin (conj x) = conj (sin x) := by
  rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← RingHom.map_mul, ← RingHom.map_mul, sinh_conj, mul_neg,
    sinh_neg, sinh_mul_I, mul_neg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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