Commit 2023-02-27 07:00 37358873

View on Github →

chore: update SHAs, forward-port (#2498) Also fix some module docstrings.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Infix.lean

added theorem List.dropSlice_sublist

added theorem List.dropSlice_subset

added theorem List.mem_of_mem_dropSlice

Modified Mathlib/Data/List/OfFn.lean

modified def List.equivSigmaTuple

added theorem List.pairwise_ofFn

Modified Mathlib/Data/Nat/Choose/Dvd.lean

Modified Mathlib/Data/Part.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/GroupTheory/GroupAction/Opposite.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/SetTheory/Lists.lean