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 or 4
• 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 + 2) is 2 ^ n.

• 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.

• ZMod.isComplement'_zpowers_unitFive_neg_one : the subgroups generated by 5 and by -1 are complements in (ZMod (2 ^ n))ˣ.

• ZMod.zpowers_mk_unitFive_eq_top : the class of 5 generates the quotient of (ZMod (2 ^ n))ˣ by ⟨-1⟩, which is thus cyclic (ZMod.isCyclic_units_two_pow_quotient_neg_one).

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)ˣ

The multiplicative group of ZMod p is cyclic.

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.

def ZMod.unitFive {n : ℕ} : (ZMod (2 ^ n))ˣ

The unit 5 of ZMod (2 ^ n).

Equations

• ZMod.unitFive = ZMod.unitOfCoprime 5 ⋯

@[simp]

theorem ZMod.coe_unitFive {n : ℕ} : ↑unitFive = 5

The value of unitFive is 5.

theorem ZMod.unitFive_eq_one {n : ℕ} (hn : n ≤ 2) : unitFive = 1

The unit 5 of ZMod (2 ^ n) is 1 when n ≤ 2.

theorem ZMod.orderOf_unitFive (n : ℕ) : orderOf unitFive = 2 ^ (n - 2)

The order of unitFive in (ZMod (2 ^ n))ˣ is 2 ^ (n - 2).

theorem ZMod.unitsMap_unitFive {m n : ℕ} (h : 2 ^ m ∣ 2 ^ n) : (unitsMap h) unitFive = unitFive

The unit 5 of ZMod (2 ^ n) maps to the unit 5 of ZMod (2 ^ m).

theorem ZMod.disjoint_zpowers_unitFive_neg_one (n : ℕ) : Disjoint (Subgroup.zpowers unitFive) (Subgroup.zpowers (-1))

The subgroups generated by 5 and by -1 in (ZMod (2 ^ n))ˣ are disjoint.

theorem ZMod.isComplement'_zpowers_unitFive_neg_one (n : ℕ) : (Subgroup.zpowers unitFive).IsComplement' (Subgroup.zpowers (-1))

The subgroups generated by 5 and by -1 are complements in (ZMod (2 ^ n))ˣ.

theorem ZMod.zpowers_mk_unitFive_eq_top (n : ℕ) : Subgroup.zpowers ↑unitFive = ⊤

The class of 5 generates the quotient of (ZMod (2 ^ n))ˣ by ⟨-1⟩.

instance ZMod.isCyclic_units_two_pow_quotient_neg_one (n : ℕ) : IsCyclic ((ZMod (2 ^ n))ˣ ⧸ Subgroup.zpowers (-1))

The quotient of (ZMod (2 ^ n))ˣ by ⟨-1⟩ is cyclic.