mathlib

3d0bb870 - feat(data/zmod/quotient): Version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption (#16175)

feat(data/zmod/quotient): Version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption (#16175) This PR adds a version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption.