Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-17 20:50 95d33ee9

View on Github →

refactor(algebra/quadratic_discriminant): drop linearity condition; cleanup (#4656) Renames:

  • discriminant_le_zero to discrim_le_zero
  • discriminant_lt_zero to discrim_lt_zero

Estimated changes

added theorem exists_le_mul_self
added theorem exists_lt_mul_self
modified def discrim
added theorem discrim_le_zero
added theorem discrim_lt_zero
deleted theorem discriminant_le_zero
deleted theorem discriminant_lt_zero
deleted theorem exist_quadratic_eq_zero
deleted theorem exists_le_mul_self
deleted theorem exists_lt_mul_self
modified theorem quadratic_eq_zero_iff