Commit 2024-07-09 08:19 860f0cb1

View on Github →

chore(Data.NNRat.Defs): reduce imports (#14541) A more straightforward proof and we can reduce the explicit imports for Data.NNRat.Defs by a third.

Estimated changes

Modified Mathlib/Data/Int/Star.lean

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/Data/Nat/Digits.lean

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

Modified Mathlib/Data/Nat/Hyperoperation.lean

Modified Mathlib/Data/Nat/Nth.lean

Modified Mathlib/Data/Num/Prime.lean

Modified Mathlib/Data/Rat/Star.lean

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

Modified scripts/noshake.json