Lean4
/-- The quotient `(ℤ ∙ a) ⧸ (stabilizer b)` is cyclic of order `minimalPeriod (a +ᵥ ·) b`. -/
noncomputable def zmultiplesQuotientStabilizerEquiv :
zmultiples a ⧸ stabilizer (zmultiples a) b ≃+ ZMod (minimalPeriod (a +ᵥ ·) b) :=
(ofBijective
(map _ (stabilizer (zmultiples a) b) (zmultiplesHom (zmultiples a) ⟨a, mem_zmultiples a⟩)
(by
rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, natCast_zsmul]
simp_rw [← vadd_iterate]
exact isPeriodicPt_minimalPeriod (a +ᵥ ·) b))
⟨by
rw [← ker_eq_bot_iff, eq_bot_iff]
refine fun q => induction_on q fun n hn => ?_
rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ← zsmul_vadd_eq_iff_minimalPeriod_dvd]
exact (eq_zero_iff _).mp hn, fun q => induction_on q fun ⟨_, n, rfl⟩ => ⟨n, rfl⟩⟩).symm.trans
(Int.quotientZMultiplesNatEquivZMod (minimalPeriod (a +ᵥ ·) b))
