IntegerMultipleSubgroup.lean

def integerMultipleSubgroup (d : ℤ) : Subgroup (Multiplicative ℤ) where
  carrier := {n | d ∣ Multiplicative.toAdd n}
  one_mem' := by
    change d ∣ (0 : ℤ)
    exact dvd_zero d
  mul_mem' := by
    intro x y hx hy
    change d ∣ Multiplicative.toAdd (x * y)
    rw [toAdd_mul]
    exact dvd_add hx hy
  inv_mem' := by
    intro x hx
    change d ∣ Multiplicative.toAdd x⁻¹
    rw [toAdd_inv]
    exact dvd_neg.mpr hx

theorem mem_integerMultipleSubgroup_iff
    (d : ℤ) (n : Multiplicative ℤ) :
    n ∈ integerMultipleSubgroup d ↔ d ∣ Multiplicative.toAdd n

theorem ofAdd_mem_integerMultipleSubgroup_iff (d n : ℤ) :
    Multiplicative.ofAdd n ∈ integerMultipleSubgroup d ↔ d ∣ n

theorem ofAdd_mul_mem_integerMultipleSubgroup (d n : ℤ) :
    Multiplicative.ofAdd (d * n) ∈ integerMultipleSubgroup d

theorem ofAdd_mul_comm_mem_integerMultipleSubgroup (d n : ℤ) :
    Multiplicative.ofAdd (n * d) ∈ integerMultipleSubgroup d

theorem integerMultipleSubgroup_le_of_dvd {a b : ℤ} (hab : a ∣ b) :
    integerMultipleSubgroup b ≤ integerMultipleSubgroup a

theorem integerMultipleSubgroup_one_eq_top :
    integerMultipleSubgroup (1 : ℤ) = ⊤

def multiplicativeIntToZModHom (d : ℤ) :
    Multiplicative ℤ →* Multiplicative (ZMod d.natAbs)

theorem multiplicativeIntToZModHom_apply
    (d : ℤ) (n : Multiplicative ℤ) :
    multiplicativeIntToZModHom d n =
      Multiplicative.ofAdd ((n.toAdd : ZMod d.natAbs))

theorem multiplicativeIntToZModHom_ker_eq_integerMultipleSubgroup (d : ℤ) :
    (multiplicativeIntToZModHom d).ker = integerMultipleSubgroup d

theorem multiplicativeIntToZModHom_surjective (d : ℤ) :
    Function.Surjective (multiplicativeIntToZModHom d)

def valueModIntegerMultipleSubgroupEquivZMod (d : ℤ) :
    Multiplicative ℤ ⧸ integerMultipleSubgroup d ≃*
      Multiplicative (ZMod d.natAbs)

theorem valueModIntegerMultipleSubgroupEquivZMod_mk
    (d n : ℤ) :
    valueModIntegerMultipleSubgroupEquivZMod d
        (QuotientGroup.mk' (integerMultipleSubgroup d)
          (Multiplicative.ofAdd n)) =
      Multiplicative.ofAdd ((n : ZMod d.natAbs))