Commit 2025-10-15 06:33 4c1ded9b

View on Github →

chore: drop Nat.Basic import from List.Basic (#30555) A slight import win for a minimal change.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

modified theorem List.getElem?_length

Modified Mathlib/Data/List/Infix.lean

Modified Mathlib/Data/List/InsertIdx.lean

Modified Mathlib/Data/List/Lex.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Zip.lean

Modified Mathlib/Data/Multiset/Defs.lean