English
The value cos(π/5) equals (1+√5)/4.
Русский
Значение cos(π/5) равно (1+√5)/4.
LaTeX
$$$\\\\cos\\\\left(\\\\frac{\\\\pi}{5}\\\\right) = \\\\frac{1+\\\\sqrt{5}}{4}$$$
Lean4
/-- The cosine of `π / 5` is `(1 + √5) / 4`. -/
@[simp]
theorem cos_pi_div_five : cos (π / 5) = (1 + √5) / 4 :=
by
set c := cos (π / 5)
have : 4 * (c * c) + (-2) * c + (-1) = 0 :=
by
rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]
exact quadratic_root_cos_pi_div_five
have hd : discrim 4 (-2) (-1) = (2 * √5) * (2 * √5) := by norm_num [discrim, mul_mul_mul_comm]
rcases (quadratic_eq_zero_iff (by simp) hd c).mp this with h | h
· simp [h]; linarith
· absurd (show 0 ≤ c from cos_nonneg_of_mem_Icc <| by constructor <;> linarith [pi_pos.le])
rw [not_le, h]
exact div_neg_of_neg_of_pos (by norm_num [lt_sqrt]) (by positivity)
