tan_pi_div_six

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

The tangent of π/6 equals 1/√3.

Русский

Тангенс π/6 равен 1/√3.

LaTeX

$$$\\\\tan\\\\left(\\\\frac{\\\\pi}{6}\\\\right) = \\\\dfrac{1}{\\\\sqrt{3}}$$$

Lean4

@[simp]
theorem tan_pi_div_six : tan (π / 6) = 1 / √3 :=
  by
  rw [tan_eq_sin_div_cos, sin_pi_div_six, cos_pi_div_six]
  ring

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

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

Разделы

Аффилиация

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