Commit 2024-05-05 04:54 c1f040b7

View on Github →

chore(Data/List/Perm): some nthLe -> get migration (#12397)

Estimated changes

Modified Mathlib/Data/List/Perm.lean

added theorem List.get_permutations'Aux

added theorem List.permutations'Aux_get_zero

deleted theorem List.permutations'Aux_nthLe_zero