mathlib3
3813d4ea - chore(data/nat/modeq): split out lemmas about lists (#18004)

Commit
3 years ago
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.
Author
Parents
Loading