mathlib

aae786c2 - feat(data/zmod/basic): fix a diamond in comm_ring and field (#14712)

feat(data/zmod/basic): fix a diamond in comm_ring and field (#14712) Before this change the following diamond existed: ```lean import data.zmod.basic variables {p : ℕ} [fact p.prime] example : @euclidean_domain.to_comm_ring _ (@field.to_euclidean_domain _ (zmod.field p)) = zmod.comm_ring p := rfl ``` as the eta-expanded `zmod.comm_ring` was not defeq to itself, as it is defined via cases. We fix this by instead defining each field by cases, which looks worse but at least seems to resolve the issue. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/zmod.20comm_ring.20field.20diamond/near/285847071 for discussion