mathlib3

c1f329df - feat(data/zmod/quotient): The quotient `<a>/stab(b)` is cyclic of order `minimal_period ((+ᵥ) a) b` (#13722)

feat(data/zmod/quotient): The quotient `<a>/stab(b)` is cyclic of order `minimal_period ((+ᵥ) a) b` (#13722) This PR adds an isomorphism stating that the quotient `<a>/stab(b)` is cyclic of order `minimal_period ((+ᵥ) a) b`. There is also a multiplicative version, but it is easily proved from the additive version, so I'll PR the multiplicative version afterwards. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>