Commit 2024-08-06 02:26 89f95eea

View on Github →

chore(Perm/List): List.get -> getElem (#15477) Deprecate List.get lemmas, use getElem versions in proofs.

Estimated changes

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Modified Mathlib/GroupTheory/Perm/List.lean

modified theorem List.formPerm_apply_getElem

modified theorem List.formPerm_pow_apply_getElem