Commit 2023-05-25 14:13 12633d21

View on Github →

feat: port Data.ZMod.Quotient (#4074)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/ZMod/Quotient.lean

added theorem AddAction.orbitZmultiplesEquiv_symm_apply'

added theorem AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply

added def Int.quotientSpanEquivZMod

added def Int.quotientSpanNatEquivZMod

added def Int.quotientZmultiplesEquivZMod

added def Int.quotientZmultiplesNatEquivZMod

added theorem IsOfFinOrder.finite_zpowers

added theorem MulAction.minimalPeriod_eq_card

added theorem MulAction.orbitZpowersEquiv_symm_apply'

added theorem MulAction.orbitZpowersEquiv_symm_apply

added theorem MulAction.zpowersQuotientStabilizerEquiv_symm_apply

added theorem order_eq_card_zpowers'