Commit 2025-06-02 06:21 a55b9761

View on Github →

feat(Perm/Fin): add lemmas about cycleRange and insertNth (#24980)

Estimated changes

Modified Mathlib/GroupTheory/Perm/Fin.lean

added theorem Fin.cons_apply_cycleRange

added theorem Fin.cons_comp_cycleRange

added theorem Fin.insertNth_apply_cycleRange_symm

added theorem Fin.insertNth_comp_cycleRange_symm