Commit 2024-08-22 13:52 24d5f11a

View on Github →

chore (GCDMonoid.Nat): avoid bundled ordered algebra and move Init.Data.Int.Order (#15152) We swap out some bundled ordered algebra API calls for native Nat and Int ones. We also add one. This allows us to avoid needing bundled ordered algebra in this file and pushes its import further downstream. Since it touches Init.Data.Int.Order, we rename it Data.Int.Order.Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GCDMonoid/Nat.lean

modified theorem Int.nonneg_of_normalize_eq_self

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Modified Mathlib/Data/Int/GCD.lean

Renamed Mathlib/Init/Data/Int/Order.lean to Mathlib/Data/Int/Order/Basic.lean

added theorem Int.mul_nonneg_of_nonneg_or_nonpos

added theorem Int.nonneg_or_nonpos_of_mul_nonneg

Modified Mathlib/Data/Nat/Factors.lean

Modified Mathlib/Data/Nat/GCD/Basic.lean

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/Data/PNat/Defs.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean

Modified Mathlib/Tactic/Positivity.lean

Modified scripts/noshake.json