sin_pi_div_six

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

sin(π / 6) = 1/2.

Русский

sin(π / 6) = 1/2.

LaTeX

$$$\\sin\\left(\\frac{\\pi}{6}\\right) = \\frac{1}{2}$$$

Lean4

/-- The sine of `π / 6` is `1 / 2`. -/
@[simp]
theorem sin_pi_div_six : sin (π / 6) = 1 / 2 :=
  by
  rw [← cos_pi_div_two_sub, ← cos_pi_div_three]
  congr
  ring

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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