Commit 2024-04-24 12:37 9150835a

View on Github →

chore(Data/List): add dates to all deprecated lemmas (#12337) Most of them go back to the port.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/Count.lean

modified theorem List.count_cons'

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Infix.lean

Modified Mathlib/Data/List/InsertNth.lean

Modified Mathlib/Data/List/Join.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/NodupEquivFin.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Pairwise.lean

modified theorem List.pairwise_map'

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/List/ToFinsupp.lean