Commit 2026-03-08 17:29 3298c0b8

View on Github →

feat: Int.mul_{pos,nonpos,neg}_iff (#36340) Completing a rectangle of lemmas.

Estimated changes

Modified Mathlib/Data/Int/Order/Basic.lean

modified theorem Int.le.elim

modified theorem Int.lt.elim

modified theorem Int.mul_nonneg_of_nonneg_or_nonpos

modified theorem Int.nonneg_or_nonpos_of_mul_nonneg