Theorem discrim_le_zero_of_nonpos

Modification history

2024-10-04 08:21
Mathlib/Algebra/QuadraticDiscriminant.lean
feat: the cosine of `π / 5` is `(1 + √5) / 4` (#17393)
Modified discrim_le_zero_of_nonposView on Github →
2023-03-18 10:25
Mathlib/Algebra/QuadraticDiscriminant.lean
feat: port Algebra.QuadraticDiscriminant (#2964)
Added discrim_le_zero_of_nonposView on Github →