Theorem discrim_lt_zero_of_neg

Modification history

2024-10-04 08:21

Mathlib/Algebra/QuadraticDiscriminant.lean

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

Modified discrim_lt_zero_of_neg View on Github →

2023-03-18 10:25

Mathlib/Algebra/QuadraticDiscriminant.lean

feat: port Algebra.QuadraticDiscriminant (#2964)

Added discrim_lt_zero_of_neg View on Github →