Commit 2024-06-12 01:24 2b37c48a

View on Github →

chore(GroupTheory/Perm/List): nthLe -> get migration (#13446) chore(GroupTheory/Perm/List): nthLe -> get migration Rewrite theorems in GroupTheory/Perm/List to use List.get. Deprecate old ones and rewrite them as thin wrappers around new ones.

Estimated changes

Modified Mathlib/GroupTheory/Perm/List.lean

modified theorem List.formPerm_apply_get

added theorem List.formPerm_apply_get_length

added theorem List.formPerm_apply_get_zero

added theorem List.formPerm_apply_lt_get

modified theorem List.formPerm_pow_apply_get