cos_sq

Mathlib.Analysis.Complex.Trigonometric

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

English

cos^2 x = 1/2 + cos(2x)/2.

Русский

cos^2 x = 1/2 + cos(2x)/2.

LaTeX

$$$\\forall x \\in \\mathbb{C},\\; \\cos x^2 = \\tfrac{1}{2} + \\tfrac{\\cos(2x)}{2}$$$

Lean4

theorem cos_sq : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 := by simp [cos_two_mul, ← add_div, mul_div_cancel_left₀, -one_div]

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

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

Разделы

Аффилиация

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