Theorem sub_mul_sub_neg_iff

Modification history

2025-05-15 03:04
Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
feat(Algebra/Order/Ring/Unbundled/Basic): add (x - a) * (x - b) positivity criterion (#24418)
Added sub_mul_sub_neg_iffView on Github →