sub_coe_pi_eq_add_coe_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

English

For any angle θ, θ − π equals θ + π.

Русский

Для любого угла θ, θ − π равно θ + π.

LaTeX

$$$ \theta - \pi = \theta + \pi $$$

Lean4

theorem sub_coe_pi_eq_add_coe_pi (θ : Angle) : θ - π = θ + π := by rw [sub_eq_add_neg, neg_coe_pi]

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

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

Разделы

Аффилиация

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