Cyclicity of the units of ZMod n

ZMod.isCyclic_units_iff : (ZMod n)ˣ is cyclic iff one of the following mutually exclusive cases happens:

• n = 0 (then ZMod 0 ≃+* ℤ and the group of units is cyclic of order 2);
• n = 1, 2 or4`
• n is a power p ^ e of an odd prime number, or twice such a power (with 1 ≤ e).

The individual cases are proved by inferInstance and are also directly provided by :

• ZMod.isCyclic_units_zero
• ZMod.isCyclic_units_one
• ZMod.isCyclic_units_two
• ZMod.isCyclic_units_four

The case of prime numbers is also an instance:

• ZMod.isCyclic_units_prime

• ZMod.not_isCyclic_units_eight: (ZMod 8)ˣ is not cyclic

• ZMod.orderOf_one_add_mul_prime: the order of 1 + a * p modulo p ^ (n + 1) is p ^ n when p does not divide a.

• ZMod.orderOf_five : the order of 5 modulo 2 ^ (n + 3) is 2 ^ (n + 1).

• ZMod.isCyclic_units_of_prime_pow : the case of odd prime powers

• ZMod.isCyclic_units_two_pow_iff : (ZMod (2 ^ n))ˣ is cyclic iff n ≤ 2.

The proofs mostly follow [Ireland and Rosen, A classical introduction to modern number theory, chapter 4] [IR90].

theorem ZMod.isCyclic_units_zero : IsCyclic (ZMod 0)ˣ

theorem ZMod.isCyclic_units_one : IsCyclic (ZMod 1)ˣ

theorem ZMod.isCyclic_units_two : IsCyclic (ZMod 2)ˣ

theorem ZMod.isCyclic_units_four : IsCyclic (ZMod 4)ˣ

theorem ZMod.isCyclic_units_prime {p : ℕ} (hp : Nat.Prime p) : IsCyclic (ZMod p)ˣ

theorem ZMod.not_isCyclic_units_eight : ¬IsCyclic (ZMod 8)ˣ

theorem ZMod.exists_one_add_mul_pow_prime_eq {R : Type u_1} [CommSemiring R] {u v : R} {p : ℕ} (hp : Nat.Prime p) (hvu : v ∣ u) (hpuv : ↑p * u * v ∣ u ^ p) (x : R) : ∃ (y : R), (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)

theorem ZMod.exists_one_add_mul_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : ℕ} {u v : R} (hp : Nat.Prime p) (hvu : v ∣ u) (hpuv : ↑p * u * v ∣ u ^ p) (x : R) (m : ℕ) : ∃ (y : R), (1 + u * x) ^ p ^ m = 1 + ↑p ^ m * u * (x + v * y)

theorem ZMod.orderOf_one_add_mul_prime_pow {p : ℕ} (hp : Nat.Prime p) (m : ℕ) (hm0 : m ≠ 0) (hpm : m + 2 ≤ p * m) (a : ℤ) (ha : ¬↑p ∣ a) (n : ℕ) : orderOf (1 + ↑p ^ m * ↑a) = p ^ n

theorem ZMod.orderOf_one_add_mul_prime {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (a : ℤ) (ha : ¬↑p ∣ a) (n : ℕ) : orderOf (1 + ↑p * ↑a) = p ^ n

theorem ZMod.orderOf_one_add_prime {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (n : ℕ) : orderOf (1 + ↑p) = p ^ n

theorem ZMod.isCyclic_units_of_prime_pow (p : ℕ) (hp : Nat.Prime p) (hp2 : p ≠ 2) (n : ℕ) : IsCyclic (ZMod (p ^ n))ˣ

If p is an odd prime, then (ZMod (p ^ n))ˣ is cyclic for all n

theorem ZMod.isCyclic_units_two_pow_iff (n : ℕ) : IsCyclic (ZMod (2 ^ n))ˣ ↔ n ≤ 2

theorem ZMod.orderOf_one_add_four_mul (a : ℤ) (ha : Odd a) (n : ℕ) : orderOf (1 + 4 * ↑a) = 2 ^ n

theorem ZMod.orderOf_five (n : ℕ) : orderOf 5 = 2 ^ n

theorem ZMod.isCyclic_units_four_mul_iff (n : ℕ) : IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

theorem ZMod.isCyclic_units_two_mul_iff_of_odd (n : ℕ) (hn : Odd n) : IsCyclic (ZMod (2 * n))ˣ ↔ IsCyclic (ZMod n)ˣ

theorem ZMod.not_isCyclic_units_of_mul_coprime (m n : ℕ) (hm : Odd m) (hm1 : m ≠ 1) (hn : Odd n) (hn1 : n ≠ 1) (hmn : m.Coprime n) : ¬IsCyclic (ZMod (m * n))ˣ

theorem ZMod.isCyclic_units_iff_of_odd {n : ℕ} (hn : Odd n) : IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

theorem ZMod.isCyclic_units_iff (n : ℕ) : IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

(ZMod n)ˣ is cyclic iff n is of the form 0, 1, 2, 4, p ^ m, or 2 * p ^ m, where p is an odd prime and 1 ≤ m.