sin_neg

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Real.sin_neg

English

The sine function is odd: sin(-x) = - sin x for all real x.

Русский

Функция синуса нечетна: для всех вещественных x выполняется sin(-x) = - sin x.

LaTeX

$$$ \sin(-x) = -\sin x $$$

Lean4

@[simp]
theorem sin_neg : sin (-x) = -sin x := by simp [sin]

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

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

Разделы

Аффилиация

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