mathlib

00d163e3 - feat(ring_theory/zmod): Criterion for `zmod` to be a reduced ring (#16998)

feat(ring_theory/zmod): Criterion for `zmod` to be a reduced ring (#16998) I couldn't find a good place for this without adding some imports, so a new file seemed appropriate. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>