Commit 2022-07-08 18:50 2d5b45c8

View on Github →

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.

Estimated changes

Modified src/algebra/char_p/basic.lean

Modified src/algebra/ne_zero.lean

Modified src/data/zmod/basic.lean

deleted theorem zmod.card

deleted def zmod

Created src/data/zmod/defs.lean

added theorem zmod.card

added def zmod

Modified src/data/zmod/quotient.lean

Modified src/ring_theory/roots_of_unity.lean