Commit 2022-12-23 11:28 3813d4ea

View on Github →

chore(data/nat/modeq): split out lemmas about lists (#18004) By splitting out some lemmas relating list-rotation and modular arithmetic, the files data.nat.modeq and data.int.modeq become portable now.

Estimated changes

Modified archive/miu_language/decision_nec.lean

Created src/data/list/modeq.lean

added theorem list.nth_rotate

added theorem list.rotate_eq_self_iff_eq_repeat

added theorem list.rotate_one_eq_self_iff_eq_repeat

added theorem list.rotate_repeat

Modified src/data/nat/modeq.lean

deleted theorem list.nth_rotate

deleted theorem list.rotate_eq_self_iff_eq_repeat

deleted theorem list.rotate_one_eq_self_iff_eq_repeat

deleted theorem list.rotate_repeat

Modified src/group_theory/perm/cycle/type.lean