Commit 2024-03-19 09:49 4bf0be48

View on Github →

chore(Mathlib/Data/List/Basic): minimize imports (#11497) Use Nat specialized theorems, and omega, where necessary to avoid needing to import the abstract ordered algebra hierarchy for basic results about List. Import graph between Mathlib.Order.Basic and Mathlib.Data.List.Basic:

before.pdf
after.pdf

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean

Modified Mathlib/Data/List/Basic.lean

modified theorem List.take_append

Modified Mathlib/Data/List/BigOperators/Basic.lean

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/EditDistance/Bounds.lean

Modified Mathlib/Data/List/Infix.lean

Modified Mathlib/Data/List/Lattice.lean

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/Seq/Seq.lean

Modified Mathlib/Data/Seq/WSeq.lean

Modified Mathlib/Data/Stream/Init.lean

Modified scripts/noshake.json