Commit 2024-10-18 06:38 319d7a37

View on Github →

chore: move NNRat APIs earlier (#17269) No need to import bundled ordered algebraic typeclasses in ring tactic now.

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Archive/Imo/Imo2013Q1.lean

Modified Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

Modified Mathlib/Algebra/Field/Rat.lean

added theorem NNRat.coe_div

added theorem NNRat.coe_inv

added theorem NNRat.den_inv_of_ne_zero

added theorem NNRat.div_def

added theorem NNRat.inv_def

added theorem NNRat.num_div_den

added theorem NNRat.num_inv_of_ne_zero

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

deleted theorem NNRat.coe_div

deleted theorem NNRat.coe_inv

deleted theorem NNRat.den_inv_of_ne_zero

deleted theorem NNRat.div_def

deleted theorem NNRat.inv_def

deleted theorem NNRat.num_inv_of_ne_zero

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

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/Finset/Density.lean

Modified Mathlib/Data/NNRat/BigOperators.lean

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/Data/NNRat/Lemmas.lean

deleted theorem NNRat.num_div_den

Modified Mathlib/Data/Nat/BitIndices.lean

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

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

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

Modified Mathlib/Data/Rat/Star.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/Tactic/Polyrith.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified test/cancel_denoms.lean

Modified test/linear_combination'.lean

Modified test/linear_combination.lean

Modified test/module.lean

Modified test/ring.lean