Theorem Int.nonneg_or_nonpos_of_mul_nonneg

Modification history

2026-03-08 17:29
Mathlib/Data/Int/Order/Basic.lean
feat: `Int.mul_{pos,nonpos,neg}_iff` (#36340) …
Modified Int.nonneg_or_nonpos_of_mul_nonnegView on Github →
2024-08-22 13:52
Mathlib/Data/Int/Order/Basic.lean
chore (GCDMonoid.Nat): avoid bundled ordered algebra and move `Init.Data.Int.Order` (#15152) …
Added Int.nonneg_or_nonpos_of_mul_nonnegView on Github →