pith. machine review for the scientific record. sign in
lemma proved tactic proof

cos_two_pi_div_three

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 102private lemma cos_two_pi_div_three : Real.cos (2 * π / 3) = -1/2 := by

proof body

Tactic-mode proof.

 103  -- 2π/3 = π - π/3, and cos(π - x) = -cos(x)
 104  have h : (2 : ℝ) * π / 3 = π - π / 3 := by ring
 105  rw [h, Real.cos_pi_sub, Real.cos_pi_div_three]
 106  norm_num
 107
 108/-- The tetrahedral angle is between 90° and 120° (in radians).
 109    90° = π/2 ≈ 1.571, 120° = 2π/3 ≈ 2.094
 110    arccos(-1/3) ≈ 1.911 -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.