sin_pi_div_two_sub

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

For all complex x, sin(π/2 − x) = cos x.

Русский

Для всех комплексных x верно sin(π/2 − x) = cos x.

LaTeX

$$$\sin\bigl(\tfrac{\pi}{2} - x\bigr) = \cos x$$$

Lean4

theorem sin_pi_div_two_sub (x : ℂ) : sin (π / 2 - x) = cos x := by simp [sub_eq_add_neg, sin_add]

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

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

Разделы

Аффилиация

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