Structure of ℤₚˣ

noncomputable def PadicInt.torsionUnits (p : ℕ) [Fact (Nat.Prime p)] : Subgroup ℤ_[p]ˣ

The subgroup of torsion elements of ℤₚˣ.

Equations

• PadicInt.torsionUnits p = CommGroup.torsion ℤ_[p]ˣ

noncomputable def PadicInt.torsionFreeUnits (p : ℕ) [Fact (Nat.Prime p)] : Subgroup ℤ_[p]ˣ

The subgroup 1 + qℤₚ of ℤₚˣ where q = 4 if p = 2, q = p if p ≠ 2.

Equations

• PadicInt.torsionFreeUnits p = (Units.map ↑(PadicInt.toZModPow (if p = 2 then 2 else 1))).ker

theorem PadicInt.mem_torsionUnits_iff (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : x ∈ torsionUnits p ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

theorem PadicInt.mem_torsionFreeUnits_iff (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : x ∈ torsionFreeUnits p ↔ (↑p ^ if p = 2 then 2 else 1) ∣ ↑x - 1

theorem PadicInt.torsionUnits_eq_rootsOfUnity (p : ℕ) [Fact (Nat.Prime p)] : torsionUnits p = rootsOfUnity (p ^ if p = 2 then 2 else 1) ℤ_[p]

theorem PadicInt.card_torsionUnits (p : ℕ) [Fact (Nat.Prime p)] : Nat.card ↥(torsionUnits p) = (p ^ if p = 2 then 2 else 1).totient

theorem PadicInt.hasEnoughRootsOfUnity_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : HasEnoughRootsOfUnity ℤ_[p] n ↔ n ∣ p ^ if p = 2 then 2 else 1

theorem PadicInt.disjoint_torsionUnits_torsionFreeUnits (p : ℕ) [Fact (Nat.Prime p)] : Disjoint (torsionUnits p) (torsionFreeUnits p)

theorem PadicInt.torsionUnits_sup_torsionFreeUnits (p : ℕ) [Fact (Nat.Prime p)] : torsionUnits p ⊔ torsionFreeUnits p = ⊤