Commit 2024-10-04 08:21 4e8b403f

View on Github →

feat: the cosine of π / 5 is (1 + √5) / 4 (#17393)

Estimated changes

Modified Mathlib/Algebra/QuadraticDiscriminant.lean

modified theorem discrim_eq_sq_of_quadratic_eq_zero

modified theorem discrim_le_zero

modified theorem discrim_le_zero_of_nonpos

modified theorem discrim_lt_zero

modified theorem discrim_lt_zero_of_neg

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added theorem Real.Polynomial.isRoot_cos_pi_div_five

added theorem Real.cos_pi_div_five

added theorem Real.quadratic_root_cos_pi_div_five

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean

Modified Mathlib/Geometry/Euclidean/Basic.lean