Theorem Int.mul_nonneg_of_nonneg_or_nonpos

Modification history

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.mul_nonneg_of_nonneg_or_nonpos View on Github →