Semigroups and comm_ring for fin

Stream: general

[Yakov Pechersky]

What's the motivation for keeping these definitions hidden and not provided as instances for fin? They're defined in data/zmod/basic but not instanced. Yet, one might still need add_assoc, add_comm, etc.

[Yakov Pechersky]

Of course one hopes that fin terms are expressed as succ or cast_succ or last, but since we have bit0 and bit1 working for fin, at least the add_semigroup should be publicly instanced

[Johan Commelin]

I think the idea is that one shouldn't use + on fin n, but only on zmod n.

[Johan Commelin]

fin n can be used as ordered gadget, but whenever the need for addition arises, zmod n should maybe be used instead...

[Yakov Pechersky]

I agree, but if I want to prove lemmas about how fin numerals behave, then I do need add_assoc and add_comm. I guess I can just add those without giving the full instance.