Theorem sub_mul_sub_nonpos_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_nonpos_iff View on Github →