Commit 2025-05-15 03:04 a19e5f28

View on Github →

feat(Algebra/Order/Ring/Unbundled/Basic): add (x - a) * (x - b) positivity criterion (#24418)

Estimated changes

added theorem sub_mul_sub_neg_iff
added theorem sub_mul_sub_nonneg_iff
added theorem sub_mul_sub_nonpos_iff
added theorem sub_mul_sub_pos_iff