Data.Zmod.Defs mathlib4#1713

Stream: mathlib4

[Ruben Van de Velde]

Would appreciate it if someone could take a look at the CommRing instance

[Eric Wieser]

Just left a comment; it looks like you discarded the mathport output in favor of the ad-hoc port?

[Eric Wieser]

My intent with the adhoc file was for it to all be deleted as soon as someone got around to actually doing the port properly; there was nothing of value in that file worth keeping that wasn't already in mathlib3.