Lean4
/-- Any element of `ZMod N` has the form `u * d` where `u` is a unit and `d` is a divisor of `N`. -/
theorem eq_unit_mul_divisor {N : ℕ} (a : ZMod N) : ∃ d : ℕ, d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * d :=
by
rcases eq_or_ne N 0 with rfl | hN
· change ℤ at a
rcases eq_or_ne a 0 with rfl | ha
· refine ⟨0, dvd_zero _, 1, isUnit_one, by rw [Nat.cast_zero, mul_zero]⟩
refine ⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩
rcases lt_or_gt_of_ne ha with h | h
· simp only [Int.sign_eq_neg_one_of_neg h, IsUnit.neg_iff, isUnit_one]
·
simp only [Int.sign_eq_one_of_pos h, isUnit_one]
-- now the interesting case
have : NeZero N :=
⟨hN⟩
-- Define `d` as the GCD of a lift of `a` and `N`.
let d := a.val.gcd N
have hd : d ≠ 0 := Nat.gcd_ne_zero_right hN
obtain ⟨a₀, (ha₀ : _ = d * _)⟩ := a.val.gcd_dvd_left N
obtain ⟨N₀, (hN₀ : _ = d * _)⟩ := a.val.gcd_dvd_right N
refine
⟨d, ⟨N₀, hN₀⟩, ?_⟩
-- Show `a` is a unit mod `N / d`.
have hu₀ : IsUnit (a₀ : ZMod N₀) :=
by
refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)
obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩
rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm, mul_comm _ p,
mul_comm _ q] at hpq
exact
⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩
-- Lift it arbitrarily to a unit mod `N`.
obtain ⟨u, hu⟩ := (unitsMap_surjective (⟨d, mul_comm d N₀ ▸ hN₀⟩ : N₀ ∣ N)) hu₀.unit
rw [unitsMap_def, ← Units.val_inj, Units.coe_map, IsUnit.unit_spec, MonoidHom.coe_coe] at hu
refine ⟨u.val, u.isUnit, ?_⟩
rw [← natCast_zmod_val a, ← natCast_zmod_val u.1, ha₀, ← Nat.cast_mul, natCast_eq_natCast_iff, mul_comm _ d,
Nat.ModEq]
simp only [hN₀, Nat.mul_mod_mul_left, Nat.mul_right_inj hd]
rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]
