isRoot_cos_pi_div_five

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.Polynomial.isRoot_cos_pi_div_five

English

cos(π/5) is a root of the polynomial 4X^2 - 2X - 1.

Русский

cos(π/5) является корнем многочлена 4X^2 - 2X - 1.

LaTeX

$$$\\cos\\left(\\frac{\\pi}{5}\\right) \\text{ является корнем }(4X^2 - 2X - 1)$$$

Lean4

theorem isRoot_cos_pi_div_five : (4 • X ^ 2 - 2 • X - C 1 : ℝ[X]).IsRoot (cos (π / 5)) := by
  simpa using quadratic_root_cos_pi_div_five

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

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

Разделы

Аффилиация

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