mathlib

2d5b45c8 - chore(data/zmod/defs): shuffle files around (#15142)

chore(data/zmod/defs): shuffle files around (#15142) This is to prepare to fix `char_p` related diamonds. No new lemmas were added, stuff was just moved around. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>