Theorem discrim_lt_zero

Modification history

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