Commit 2023-02-21 06:50 f9c61018

View on Github →

fix: undeprecate List.get_mono and List.get_strictMono (#2308) I see no reason for these lemmas to be deprecated.

Estimated changes

Modified Mathlib/Data/List/NodupEquivFin.lean

modified def List.Nodup.getEquiv

modified def List.Sorted.getIso

modified theorem List.Sorted.get_mono

modified theorem List.Sorted.get_strictMono