Commit 2023-03-18 10:25 55d8691a

View on Github →

feat: port Algebra.QuadraticDiscriminant (#2964)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/QuadraticDiscriminant.lean

added def discrim

added theorem discrim_eq_sq_of_quadratic_eq_zero

added theorem discrim_le_zero

added theorem discrim_le_zero_of_nonpos

added theorem discrim_lt_zero

added theorem discrim_lt_zero_of_neg

added theorem discrim_neg

added theorem exists_quadratic_eq_zero

added theorem quadratic_eq_zero_iff

added theorem quadratic_eq_zero_iff_discrim_eq_sq

added theorem quadratic_eq_zero_iff_of_discrim_eq_zero

added theorem quadratic_ne_zero_of_discrim_ne_sq