Commit 2024-06-04 04:05 0128f950

View on Github →

chore: Move Data.Rat.Order to Algebra.Order.Ring.Rat (#13169)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Field/Rat.lean

Renamed Mathlib/Data/Rat/Order.lean to Mathlib/Algebra/Order/Ring/Rat.lean

deleted theorem Rat.num_nonneg

Modified Mathlib/Algebra/Ring/Rat.lean

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

Modified Mathlib/Data/Int/Defs.lean

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

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/Data/Nat/Cast/WithTop.lean

Modified Mathlib/Data/Nat/Order/Lemmas.lean

Modified Mathlib/Data/Rat/Cast/Order.lean

Modified Mathlib/Data/Rat/Defs.lean

added theorem Rat.num_nonneg

Modified Mathlib/Data/Rat/Denumerable.lean

Modified Mathlib/Data/Rat/Sqrt.lean

Modified Mathlib/NumberTheory/ADEInequality.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

Modified Mathlib/Tactic/Qify.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified test/ValuedCSP.lean

Modified test/linarith.lean