sign_pi_add

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

English

Equivalently, sign(π + θ) = - sign(θ).

Русский

Эквивалентно: sign(π + θ) = - sign(θ).

LaTeX

$$$ \text{sign}(\pi + \theta) = -\text{sign}(\theta) $$$

Lean4

@[simp]
theorem sign_pi_add (θ : Angle) : ((π : Angle) + θ).sign = -θ.sign := by rw [add_comm, sign_add_pi]

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

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

Разделы

Аффилиация

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