Commit 2023-10-15 23:39 a33e3ec1

View on Github →

chore: bump std (#7694) Some deleted lemmas have been upstreamed to Std. Note that the statements of List.zipWith_map_left (and _right) have been changed, requiring slight changes here.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.findIdx_cons

deleted theorem List.findIdx_nil

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Zip.lean

deleted theorem List.zipWith_map

deleted theorem List.zipWith_map_left

deleted theorem List.zipWith_map_right

deleted theorem List.zip_map

deleted theorem List.zip_map_left

deleted theorem List.zip_map_right

Modified Mathlib/Data/Nat/Digits.lean

Modified Mathlib/SetTheory/Lists.lean

Modified lake-manifest.json