Commit 2021-03-29 20:11 50225dad
View on Github →feat(data/fin): fin n.succ is an add_comm_group (#6898)
This just moves the proof out of data.zmod basic.
Moving the full ring instance is left for future work, as modeq, used to prove left_distrib, is not available to import in data/fin/basic.
Note this adds an import of data.int.basic to data.fin.basic. I think this is probably acceptable?