Structure of ℤₚˣ

• PadicInt.torsionfreeUnitsExponent: the smallest integer n such that the subgroup 1 + pⁿℤₚ of ℤₚˣ is torsion-free. More explicitly, n = 2 if p = 2, and n = 1 otherwise.
• PadicInt.teichmuller: the Teichmüller map (ℤ/pⁿℤ)ˣ →* ℤₚˣ where n = 2 if p = 2, and n = 1 otherwise, which maps a to the unique ϕ(pⁿ)-th roots of unity (PadicInt.torsionUnits_eq_torsion shows that it is indeed the unique roots of unity) in ℤₚ such that it is congruent to a modulo pⁿ.
• PadicInt.principalUnits p n: the subgroup 1 + pⁿℤₚ of ℤₚˣ.
• PadicInt.torsionfreeUnits: the subgroup 1 + pⁿℤₚ of ℤₚˣ where n = 2 if p = 2, and n = 1 otherwise.
• PadicInt.torsionUnits: the subgroup (ℤₚˣ)ₜₒᵣ of torsion elements of ℤₚˣ. Note that for definitionally equal reason, its actual definition is the image of the Teichmüller map (PadicInt.teichmuller). PadicInt.torsionUnits_eq_torsion shows that it is indeed equal to the set of torsion elements of ℤₚˣ.
• PadicInt.unitsContinuousEquivTorsionfreeProdTorsion: the natural continuous group isomorphism ℤₚˣ ≃ (1 + pⁿℤₚ) × (ℤₚˣ)ₜₒᵣ, where n = 2 if p = 2, and n = 1 otherwise.
• PadicInt.torsionfreeZModPowUnits p n: the subgroup 1 + pᵏℤ of (ℤ/pⁿ⁺ᵏℤ)ˣ where k = 2 if p = 2, and k = 1 otherwise.
• PadicInt.torsionfreeZModPowUnits.generator p n: the element 1 + pᵏ in the subgroup 1 + pᵏℤ of (ℤ/pⁿ⁺ᵏℤ)ˣ where k = 2 if p = 2, and k = 1 otherwise.
• PadicInt.equivTorsionfreeUnits.toFun: the map ℤₚ → ℤₚ by sending x to the limit of (1 + pᵏ) ^ (x mod pⁿ) as n → ∞, where k = 2 if p = 2, and k = 1 otherwise.
• PadicInt.equivTorsionfreeUnits: the continuous group isomorphism (ℤₚ, +) ≃ (1 + pᵏℤₚ, *) by sending x to the limit of (1 + pᵏ) ^ (x mod pⁿ) as n → ∞, where k = 2 if p = 2, and k = 1 otherwise.

Teichmüller map

def PadicInt.torsionfreeUnitsExponent (p : ℕ) : ℕ

The smallest integer n such that the subgroup 1 + pⁿℤₚ of ℤₚˣ is torsion-free. More explicitly, n = 2 if p = 2, and n = 1 otherwise.

Equations

• PadicInt.torsionfreeUnitsExponent p = if p = 2 then 2 else 1

theorem PadicInt.torsionfreeUnitsExponent_ne_zero (p : ℕ) : torsionfreeUnitsExponent p ≠ 0

theorem PadicInt.two_lt_p_pow_torsionfreeUnitsExponent (p : ℕ) [Fact (Nat.Prime p)] : 2 < p ^ torsionfreeUnitsExponent p

theorem PadicInt.even_totient_p_pow_torsionfreeUnitsExponent (p : ℕ) [Fact (Nat.Prime p)] : Even (p ^ torsionfreeUnitsExponent p).totient

theorem PadicInt.two_le_totient_p_pow_torsionfreeUnitsExponent (p : ℕ) [Fact (Nat.Prime p)] : 2 ≤ (p ^ torsionfreeUnitsExponent p).totient

theorem PadicInt.existsUnique_pow_eq_one_and_unitsMap_toZModPow_one_eq (p : ℕ) [Fact (Nat.Prime p)] (x : (ZMod (p ^ 1))ˣ) : ∃! y : ℤ_[p]ˣ, y ^ (p - 1) = 1 ∧ (Units.map ↑(toZModPow 1)) y = x

theorem PadicInt.existsUnique_pow_eq_one_and_unitsMap_toZModPow_torsionfreeUnitsExponent_eq (p : ℕ) [Fact (Nat.Prime p)] (x : (ZMod (p ^ torsionfreeUnitsExponent p))ˣ) : ∃! y : ℤ_[p]ˣ, y ^ (p ^ torsionfreeUnitsExponent p).totient = 1 ∧ (Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) y = x

noncomputable def PadicInt.teichmuller (p : ℕ) [Fact (Nat.Prime p)] : (ZMod (p ^ torsionfreeUnitsExponent p))ˣ →* ℤ_[p]ˣ

The Teichmüller map (ℤ/pⁿℤ)ˣ →* ℤₚˣ where n = 2 if p = 2, and n = 1 otherwise, which maps a to the unique ϕ(pⁿ)-th roots of unity (later we will show that in fact it is the unique roots of unity) in ℤₚ such that it is congruent to a modulo pⁿ.

Equations

• PadicInt.teichmuller p = { toFun := fun (x : (ZMod (p ^ PadicInt.torsionfreeUnitsExponent p))ˣ) => ⋯.choose, map_one' := ⋯, map_mul' := ⋯ }

theorem PadicInt.teichmuller_spec (p : ℕ) [Fact (Nat.Prime p)] (x : (ZMod (p ^ torsionfreeUnitsExponent p))ˣ) : (teichmuller p) x ^ (p ^ torsionfreeUnitsExponent p).totient = 1 ∧ (Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) ((teichmuller p) x) = x

theorem PadicInt.teichmuller_unique (p : ℕ) [Fact (Nat.Prime p)] {x : (ZMod (p ^ torsionfreeUnitsExponent p))ˣ} {y : ℤ_[p]ˣ} (hy1 : y ^ (p ^ torsionfreeUnitsExponent p).totient = 1) (hy2 : (Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) y = x) : (teichmuller p) x = y

theorem PadicInt.teichmuller_unitsMap_toZModPow_apply_eq_self_of_pow_eq_one (p : ℕ) [Fact (Nat.Prime p)] {x : ℤ_[p]ˣ} (hx : x ^ (p ^ torsionfreeUnitsExponent p).totient = 1) : (teichmuller p) ((Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) x) = x

@[simp]

theorem PadicInt.teichmuller_neg (p : ℕ) [Fact (Nat.Prime p)] (x : (ZMod (p ^ torsionfreeUnitsExponent p))ˣ) : (teichmuller p) (-x) = -(teichmuller p) x

theorem PadicInt.teichmuller_injective (p : ℕ) [Fact (Nat.Prime p)] : Function.Injective ⇑(teichmuller p)

theorem PadicInt.unitsMap_toZModPow_comp_teichmuller (p : ℕ) [Fact (Nat.Prime p)] : (Units.map ↑(toZModPow (torsionfreeUnitsExponent p))).comp (teichmuller p) = MonoidHom.id (ZMod (p ^ torsionfreeUnitsExponent p))ˣ

theorem PadicInt.leftInverse_unitsMap_toZModPow_teichmuller (p : ℕ) [Fact (Nat.Prime p)] : Function.LeftInverse ⇑(Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) ⇑(teichmuller p)

theorem PadicInt.isOpen_ker_unitsMap_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsOpen ↑(Units.map ↑(toZModPow n)).ker

theorem PadicInt.continuous_teichmuller_comp_unitsMap_toZModPow (p : ℕ) [Fact (Nat.Prime p)] : Continuous ⇑((teichmuller p).comp (Units.map ↑(toZModPow (torsionfreeUnitsExponent p))))

Subgroups of ℤₚˣ

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

The subgroup 1 + pⁿℤₚ of ℤₚˣ.

Equations

• PadicInt.principalUnits p n = (Units.map ↑(PadicInt.toZModPow n)).ker

theorem PadicInt.index_principalUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (principalUnits p n).index = (p ^ n).totient

instance PadicInt.finiteIndex_principalUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (principalUnits p n).FiniteIndex

@[simp]

theorem PadicInt.principalUnits_zero (p : ℕ) [Fact (Nat.Prime p)] : principalUnits p 0 = ⊤

@[simp]

theorem PadicInt.principalUnits_two_one : principalUnits 2 1 = ⊤

theorem PadicInt.mem_principalUnits_iff_coe_sub_one_mem (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]ˣ) : x ∈ principalUnits p n ↔ ↑x - 1 ∈ RingHom.ker (toZModPow n)

theorem PadicInt.isOpen_principalUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsOpen ↑(principalUnits p n)

theorem PadicInt.antitone_principalUnits (p : ℕ) [Fact (Nat.Prime p)] : Antitone (principalUnits p)

theorem PadicInt.units_nhds_one_hasAntitoneBasis_principalUnits (p : ℕ) [Fact (Nat.Prime p)] : (nhds 1).HasAntitoneBasis fun (n : ℕ) => ↑(principalUnits p n)

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

The subgroup 1 + pⁿℤₚ of ℤₚˣ where n = 2 if p = 2, and n = 1 otherwise.

Equations

• PadicInt.torsionfreeUnits p = PadicInt.principalUnits p (PadicInt.torsionfreeUnitsExponent p)

theorem PadicInt.index_torsionfreeUnits (p : ℕ) [Fact (Nat.Prime p)] : (torsionfreeUnits p).index = (p ^ torsionfreeUnitsExponent p).totient

instance PadicInt.finiteIndex_torsionfreeUnits (p : ℕ) [Fact (Nat.Prime p)] : (torsionfreeUnits p).FiniteIndex

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

The subgroup (ℤₚˣ)ₜₒᵣ of torsion elements of ℤₚˣ. Note that for definitionally equal reason, its actual definition is the image of the Teichmüller map. Later we will show that it is indeed equal to the set of torsion elements of ℤₚˣ.

Equations

• PadicInt.torsionUnits p = (PadicInt.teichmuller p).range

noncomputable def PadicInt.unitsContinuousEquivTorsionfreeProdTorsion (p : ℕ) [Fact (Nat.Prime p)] : ℤ_[p]ˣ ≃ₜ* ↥(torsionfreeUnits p) × ↥(torsionUnits p)

The natural continuous group isomorphism ℤₚˣ ≃ (1 + pⁿℤₚ) × (ℤₚˣ)ₜₒᵣ, where n = 2 if p = 2, and n = 1 otherwise.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PadicInt.val_fst_unitsContinuousEquivTorsionfreeProdTorsion_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : ↑((unitsContinuousEquivTorsionfreeProdTorsion p) x).1 = x * ((teichmuller p) ((Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) x))⁻¹

@[simp]

theorem PadicInt.val_snd_unitsContinuousEquivTorsionfreeProdTorsion_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : ↑((unitsContinuousEquivTorsionfreeProdTorsion p) x).2 = (teichmuller p) ((Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) x)

@[simp]

theorem PadicInt.unitsContinuousEquivTorsionfreeProdTorsion_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(torsionfreeUnits p) × ↥(torsionUnits p)) : (unitsContinuousEquivTorsionfreeProdTorsion p).symm x = ↑x.1 * ↑x.2

theorem PadicInt.units_eq_unitsContinuousEquivTorsionfreeProdTorsion_mul (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : x = ↑((unitsContinuousEquivTorsionfreeProdTorsion p) x).1 * ↑((unitsContinuousEquivTorsionfreeProdTorsion p) x).2

@[simp]

theorem PadicInt.fst_unitsContinuousEquivTorsionfreeProdTorsion_eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : ((unitsContinuousEquivTorsionfreeProdTorsion p) x).1 = 1 ↔ x ∈ torsionUnits p

@[simp]

theorem PadicInt.snd_unitsContinuousEquivTorsionfreeProdTorsion_eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]ˣ) : ((unitsContinuousEquivTorsionfreeProdTorsion p) x).2 = 1 ↔ x ∈ torsionfreeUnits p

theorem PadicInt.torsionUnits_eq_rootsOfUnity (p : ℕ) [Fact (Nat.Prime p)] : torsionUnits p = rootsOfUnity (p ^ torsionfreeUnitsExponent p).totient ℤ_[p]

theorem PadicInt.torsionUnits_le_torsion (p : ℕ) [Fact (Nat.Prime p)] : torsionUnits p ≤ CommGroup.torsion ℤ_[p]ˣ

theorem PadicInt.card_torsionUnits (p : ℕ) [Fact (Nat.Prime p)] : Nat.card ↥(torsionUnits p) = (p ^ torsionfreeUnitsExponent p).totient

instance PadicInt.finite_torsionUnits (p : ℕ) [Fact (Nat.Prime p)] : Finite ↥(torsionUnits p)

@[simp]

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

@[simp]

theorem PadicInt.disjoint_principalUnits_torsionUnits_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Disjoint (principalUnits p n) (torsionUnits p) ↔ torsionfreeUnitsExponent p ≤ n

theorem PadicInt.disjoint_torsionfreeUnits_torsionUnits (p : ℕ) [Fact (Nat.Prime p)] : Disjoint (torsionfreeUnits p) (torsionUnits p)

@[simp]

theorem PadicInt.cardinalMk_units_eq_continuum (p : ℕ) [Fact (Nat.Prime p)] : Cardinal.mk ℤ_[p]ˣ = Cardinal.continuum

theorem PadicInt.not_isCyclic_units (p : ℕ) [Fact (Nat.Prime p)] : ¬IsCyclic ℤ_[p]ˣ

The subgroup 1 + pᵏℤ of (ℤ/pⁿ⁺ᵏℤ)ˣ where k = 2 if p = 2, and k = 1 otherwise

noncomputable def PadicInt.torsionfreeZModPowUnits (p n : ℕ) : Subgroup (ZMod (p ^ (n + torsionfreeUnitsExponent p)))ˣ

The subgroup 1 + pᵏℤ of (ℤ/pⁿ⁺ᵏℤ)ˣ where k = 2 if p = 2, and k = 1 otherwise.

Equations

• PadicInt.torsionfreeZModPowUnits p n = (ZMod.unitsMap ⋯).ker

theorem PadicInt.torsionfreeUnits_eq_comap_torsionfreeZModPowUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : torsionfreeUnits p = Subgroup.comap (Units.map ↑(toZModPow (n + torsionfreeUnitsExponent p))) (torsionfreeZModPowUnits p n)

@[simp]

theorem PadicInt.card_torsionfreeZModPowUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Nat.card ↥(torsionfreeZModPowUnits p n) = p ^ n

The element 1 + pᵏ in (ℤ/pⁿ⁺ᵏℤ)ˣ where k = 2 if p = 2, and k = 1 otherwise

theorem PadicInt.isUnit_one_add_pow_torsionfreeUnitsExponent_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsUnit (1 + ↑p ^ torsionfreeUnitsExponent p)

theorem PadicInt.one_add_pow_torsionfreeUnitsExponent_toZModPow_mem_torsionfreeZModPowUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : ⋯.unit ∈ torsionfreeZModPowUnits p n

@[simp]

theorem PadicInt.orderOf_one_add_pow_torsionfreeUnitsExponent_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : orderOf (1 + ↑p ^ torsionfreeUnitsExponent p) = p ^ n

theorem PadicInt.isOfFinOrder_one_add_pow_torsionfreeUnitsExponent_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsOfFinOrder (1 + ↑p ^ torsionfreeUnitsExponent p)

noncomputable def PadicInt.torsionfreeZModPowUnits.generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : ↥(torsionfreeZModPowUnits p n)

The element 1 + pᵏ in the subgroup 1 + pᵏℤ of (ℤ/pⁿ⁺ᵏℤ)ˣ where k = 2 if p = 2, and k = 1 otherwise.

Equations

• PadicInt.torsionfreeZModPowUnits.generator p n = ⟨⋯.unit, ⋯⟩

@[simp]

theorem PadicInt.torsionfreeZModPowUnits.coe_generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : ↑(generator p n) = ⋯.unit

@[simp]

theorem PadicInt.torsionfreeZModPowUnits.orderOf_generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : orderOf (generator p n) = p ^ n

theorem PadicInt.torsionfreeZModPowUnits.isOfFinOrder_generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsOfFinOrder (generator p n)

theorem PadicInt.torsionfreeZModPowUnits.zpowers_generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Subgroup.zpowers (generator p n) = ⊤

instance PadicInt.torsionfreeZModPowUnits.isCyclic (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsCyclic ↥(torsionfreeZModPowUnits p n)

theorem PadicInt.torsionfreeZModPowUnits.generator_spec (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (x : ↥(torsionfreeZModPowUnits p n)) : ∃! i : ℕ, i < p ^ n ∧ generator p n ^ i = x

The isomorphism (1 + pⁿℤₚ, *) ≃ (ℤₚ, +)

theorem PadicInt.val_toZModPow_eq_appr (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) (i : ℕ) : ((toZModPow i) x).val = x.appr i

theorem PadicInt.pow_succ_dvd_one_add_pow_pow_pow_pow_sub_one (p : ℕ) [Fact (Nat.Prime p)] (n i : ℕ) : ↑p ^ (i + 1) ∣ ((1 + ↑p ^ torsionfreeUnitsExponent p) ^ n) ^ p ^ i - 1

theorem PadicInt.equivTorsionfreeUnits.toFun_aux (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) (i : ℕ) : ↑p ^ i ∣ (1 + ↑p ^ torsionfreeUnitsExponent p) ^ x.appr (i + 1) - (1 + ↑p ^ torsionfreeUnitsExponent p) ^ x.appr i

noncomputable def PadicInt.equivTorsionfreeUnits.toFun (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : ℤ_[p]

The map ℤₚ → ℤₚ by sending x to the limit of (1 + pᵏ) ^ (x mod pⁿ) as n → ∞, where k = 2 if p = 2, and k = 1 otherwise.

Equations

• PadicInt.equivTorsionfreeUnits.toFun p x = PadicInt.ofIntSeq (fun (i : ℕ) => (1 + ↑p ^ PadicInt.torsionfreeUnitsExponent p) ^ x.appr i) ⋯

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toZModPow_toFun (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) (i : ℕ) : (toZModPow i) (toFun p x) = (1 + ↑p ^ torsionfreeUnitsExponent p) ^ x.appr i

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_natCast (p : ℕ) [Fact (Nat.Prime p)] (x : ℕ) : toFun p ↑x = (1 + ↑p ^ torsionfreeUnitsExponent p) ^ x

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_zero (p : ℕ) [Fact (Nat.Prime p)] : toFun p 0 = 1

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_one (p : ℕ) [Fact (Nat.Prime p)] : toFun p 1 = 1 + ↑p ^ torsionfreeUnitsExponent p

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_add (p : ℕ) [Fact (Nat.Prime p)] (x y : ℤ_[p]) : toFun p (x + y) = toFun p x * toFun p y

theorem PadicInt.equivTorsionfreeUnits.isUnit_toFun (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : IsUnit (toFun p x)

theorem PadicInt.equivTorsionfreeUnits.toFun_mem_principalUnits_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : ⋯.unit ∈ principalUnits p (n + torsionfreeUnitsExponent p) ↔ x ∈ Ideal.span {↑p ^ n}

theorem PadicInt.equivTorsionfreeUnits.toFun_mem_torsionfreeUnits (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : ⋯.unit ∈ torsionfreeUnits p

theorem PadicInt.equivTorsionfreeUnits.toFun_injective (p : ℕ) [Fact (Nat.Prime p)] : Function.Injective (toFun p)

theorem PadicInt.equivTorsionfreeUnits.toFun_surjective (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(torsionfreeUnits p)) : ∃ (y : ℤ_[p]), toFun p y = ↑↑x

noncomputable def PadicInt.equivTorsionfreeUnits (p : ℕ) [Fact (Nat.Prime p)] : Multiplicative ℤ_[p] ≃ₜ* ↥(torsionfreeUnits p)

The continuous group isomorphism (ℤₚ, +) ≃ (1 + pᵏℤₚ, *) by sending x to the limit of (1 + pᵏ) ^ (x mod pⁿ) as n → ∞, where k = 2 if p = 2, and k = 1 otherwise.

Equations

• PadicInt.equivTorsionfreeUnits p = { toEquiv := Equiv.ofBijective (fun (x : Multiplicative ℤ_[p]) => ⟨⋯.unit, ⋯⟩) ⋯, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem PadicInt.coe_equivTorsionfreeUnits_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : ↑↑((equivTorsionfreeUnits p) x) = equivTorsionfreeUnits.toFun p x

Further results of torsionUnits

theorem PadicInt.torsionUnits_eq_torsion (p : ℕ) [Fact (Nat.Prime p)] : torsionUnits p = CommGroup.torsion ℤ_[p]ˣ

theorem PadicInt.hasEnoughRootsOfUnity_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : HasEnoughRootsOfUnity ℤ_[p] n ↔ n ∣ (p ^ torsionfreeUnitsExponent p).totient

instance PadicInt.hasEnoughRootsOfUnity_sub_one (p : ℕ) [Fact (Nat.Prime p)] : HasEnoughRootsOfUnity ℤ_[p] (p - 1)

Closed subgroups of ℤₚˣ

theorem PadicInt.finite_or_finiteIndex_of_subgroup_units_of_isClosed (p : ℕ) [Fact (Nat.Prime p)] (G : Subgroup ℤ_[p]ˣ) (hG : IsClosed ↑G) : (↑G).Finite ∧ G ≤ torsionUnits p ∨ G.FiniteIndex ∧ IsOpen ↑G

A closed subgroup of ℤₚˣ is either finite or is of finite index.

theorem CommGroup.torsion_le_comap_torsion {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (f : G →* H) : torsion G ≤ Subgroup.comap f (torsion H)

TODO: go to mathlib

theorem AddCommGroup.torsion_le_comap_torsion {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (f : G →+ H) : torsion G ≤ AddSubgroup.comap f (torsion H)

theorem CommGroup.torsion_eq_comap_torsion_of_finite_ker {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (f : G →* H) [Finite ↥f.ker] : torsion G = Subgroup.comap f (torsion H)

TODO: go to mathlib

theorem AddCommGroup.torsion_eq_comap_torsion_of_finite_ker {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (f : G →+ H) [Finite ↥f.ker] : torsion G = AddSubgroup.comap f (torsion H)

theorem PadicInt.nonempty_continuousMulEquiv_of_continuousMonoidHom_units_of_finite_ker (p : ℕ) [Fact (Nat.Prime p)] (G : Type u_1) [Infinite G] [CommGroup G] [TopologicalSpace G] [CompactSpace G] (f : G →ₜ* ℤ_[p]ˣ) [Finite ↥f.ker] : Nonempty (G ⧸ CommGroup.torsion G ≃ₜ* Multiplicative ℤ_[p])

If there is a continuous group homomorphism from an infinite compact topological group G to ℤₚˣ with finite kernel, then G / Gₜₒᵣ ≃ ℤₚ.

theorem PadicInt.nonempty_continuousMulEquiv_of_continuousMonoidHom_units_of_injective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u_1) [Infinite G] [CommGroup G] [TopologicalSpace G] [CompactSpace G] (f : G →ₜ* ℤ_[p]ˣ) (hf : Function.Injective ⇑f) : Nonempty (G ⧸ CommGroup.torsion G ≃ₜ* Multiplicative ℤ_[p])

If there is a continuous group embedding from an infinite compact topological group G to ℤₚˣ, then G / Gₜₒᵣ ≃ ℤₚ.