Theorem Int.nonneg_or_nonpos_of_mul_nonneg

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