Structure of `ℤₚˣ` #

If a surjective group homomorphism f : B →* C has a section g : C →* B, then there is a natural isomorphism of B to ker(f) × im(g). We use im(g) instead of C since if B has topology, then both of ker(f) and im(g) will also get topology automatically.

Equations

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

Instances For

source

@[simp]

theorem MonoidHom.val_fst_equivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) (x : B) :

↑((f.equivKerProdRangeOfLeftInverse g hfg) x).1 = x * (g (f x))⁻¹

source

@[simp]

theorem MonoidHom.val_snd_equivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) (x : B) :

↑((f.equivKerProdRangeOfLeftInverse g hfg) x).2 = g (f x)

source

@[simp]

theorem MonoidHom.equivKerProdRangeOfLeftInverse_symm_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) (x : ↥f.ker × ↥g.range) :

(f.equivKerProdRangeOfLeftInverse g hfg).symm x = ↑x.1 * ↑x.2

source

theorem MonoidHom.continuous_equivKerProdRangeOfLeftInverse_symm {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [ContinuousMul B] :

Continuous ⇑(f.equivKerProdRangeOfLeftInverse g hfg).symm

source

theorem MonoidHom.continuous_equivKerProdRangeOfLeftInverse {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) :

Continuous ⇑(f.equivKerProdRangeOfLeftInverse g hfg)

source

def MonoidHom.continuousEquivKerProdRangeOfLeftInverse {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) :

B ≃ₜ* ↥f.ker × ↥g.range

Continuous version of equivKerProdRangeOfLeftInverse.

Equations

f.continuousEquivKerProdRangeOfLeftInverse g hfg hc = { toMulEquiv := f.equivKerProdRangeOfLeftInverse g hfg, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem MonoidHom.val_fst_continuousEquivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) (x : B) :

↑((f.continuousEquivKerProdRangeOfLeftInverse g hfg hc) x).1 = x * (g (f x))⁻¹

source

@[simp]

theorem MonoidHom.val_snd_continuousEquivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) (x : B) :

↑((f.continuousEquivKerProdRangeOfLeftInverse g hfg hc) x).2 = g (f x)

source

@[simp]

theorem MonoidHom.continuousEquivKerProdRangeOfLeftInverse_symm_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) (x : ↥f.ker × ↥g.range) :

(f.continuousEquivKerProdRangeOfLeftInverse g hfg hc).symm x = ↑x.1 * ↑x.2

source

instance PadicInt.isLocalHom_toZMod (p : ℕ) [Fact (Nat.Prime p)] :

IsLocalHom toZMod

source

theorem PadicInt.zmod_cast_comp_toZModPow_eq_toZMod (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (h : n ≠ 0) :

(ZMod.castHom ⋯ (ZMod p)).comp (toZModPow n) = toZMod

source

instance PadicInt.isLocalHom_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [NeZero n] :

IsLocalHom (toZModPow n)

source

theorem PadicInt.unitsMap_toZMod_surjective (p : ℕ) [Fact (Nat.Prime p)] :

Function.Surjective ⇑(Units.map ↑toZMod)

source

theorem PadicInt.unitsMap_toZModPow_surjective (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Function.Surjective ⇑(Units.map ↑(toZModPow n))

Some silly results for `ZMod` #

source

theorem ZMod.units_eq_one_of_eq_two {q : ℕ} (hq : q = 2) (x : (ZMod q)ˣ) :

x = 1

source

theorem ZMod.units_eq_one_or_neg_one_of_eq_three {q : ℕ} (hq : q = 3) (x : (ZMod q)ˣ) :

x = 1 ∨ x = -1

source

theorem ZMod.units_eq_one_or_neg_one_of_eq_four {q : ℕ} (hq : q = 4) (x : (ZMod q)ˣ) :

x = 1 ∨ x = -1

source

theorem ZMod.units_eq_one_or_neg_one_of_eq_six {q : ℕ} (hq : q = 6) (x : (ZMod q)ˣ) :

x = 1 ∨ x = -1

source

theorem ZMod.eq_one_of_eq_two_of_isUnit {q : ℕ} (hq : q = 2) (x : ZMod q) (hx : IsUnit x) :

x = 1

source

theorem ZMod.eq_one_or_neg_one_of_eq_three_of_isUnit {q : ℕ} (hq : q = 3) (x : ZMod q) (hx : IsUnit x) :

x = 1 ∨ x = -1

source

theorem ZMod.eq_one_or_neg_one_of_eq_four_of_isUnit {q : ℕ} (hq : q = 4) (x : ZMod q) (hx : IsUnit x) :

x = 1 ∨ x = -1

source

theorem ZMod.eq_one_or_neg_one_of_eq_six_of_isUnit {q : ℕ} (hq : q = 6) (x : ZMod q) (hx : IsUnit x) :

x = 1 ∨ x = -1

Teichmüller map #

source

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

Instances For

source

theorem PadicInt.torsionfreeUnitsExponent_ne_zero (p : ℕ) :

torsionfreeUnitsExponent p ≠ 0

source

theorem PadicInt.two_lt_p_pow_torsionfreeUnitsExponent (p : ℕ) [Fact (Nat.Prime p)] :

2 < p ^ torsionfreeUnitsExponent p

source

theorem PadicInt.even_totient_p_pow_torsionfreeUnitsExponent (p : ℕ) [Fact (Nat.Prime p)] :

Even (p ^ torsionfreeUnitsExponent p).totient

source

theorem PadicInt.two_le_totient_p_pow_torsionfreeUnitsExponent (p : ℕ) [Fact (Nat.Prime p)] :

2 ≤ (p ^ torsionfreeUnitsExponent p).totient

source

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

source

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

source

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' := ⋯ }

Instances For

source

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

source

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

source

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

source

@[simp]

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

(teichmuller p) (-x) = -(teichmuller p) x

source

theorem PadicInt.teichmuller_injective (p : ℕ) [Fact (Nat.Prime p)] :

Function.Injective ⇑(teichmuller p)

source

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

source

theorem PadicInt.leftInverse_unitsMap_toZModPow_teichmuller (p : ℕ) [Fact (Nat.Prime p)] :

Function.LeftInverse ⇑(Units.map ↑(toZModPow (torsionfreeUnitsExponent p))) ⇑(teichmuller p)

source

theorem PadicInt.isOpen_ker_unitsMap_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

IsOpen ↑(Units.map ↑(toZModPow n)).ker

source

theorem PadicInt.continuous_teichmuller_comp_unitsMap_toZModPow (p : ℕ) [Fact (Nat.Prime p)] :

Continuous ⇑((teichmuller p).comp (Units.map ↑(toZModPow (torsionfreeUnitsExponent p))))

Subgroups of `ℤₚˣ` #

source

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

Instances For

source

@[simp]

theorem PadicInt.principalUnits_zero (p : ℕ) [Fact (Nat.Prime p)] :

principalUnits p 0 = ⊤

source

@[simp]

theorem PadicInt.principalUnits_two_one :

principalUnits 2 1 = ⊤

source

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)

source

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

IsOpen ↑(principalUnits p n)

source

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

Antitone (principalUnits p)

source

theorem PadicInt.units_nhds_one_hasAntitoneBasis_principalUnits (p : ℕ) [Fact (Nat.Prime p)] :

(nhds 1).HasAntitoneBasis fun (n : ℕ) => ↑(principalUnits p n)

source

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)

Instances For

source

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

Instances For

source

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.

Instances For

source

@[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))⁻¹

source

@[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)

source

@[simp]

theorem PadicInt.unitsContinuousEquivTorsionfreeProdTorsion_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(torsionfreeUnits p) × ↥(torsionUnits p)) :

(unitsContinuousEquivTorsionfreeProdTorsion p).symm x = ↑x.1 * ↑x.2

source

theorem PadicInt.torsionUnits_eq_rootsOfUnity (p : ℕ) [Fact (Nat.Prime p)] :

torsionUnits p = rootsOfUnity (p ^ torsionfreeUnitsExponent p).totient ℤ_[p]

source

theorem PadicInt.torsionUnits_le_torsion (p : ℕ) [Fact (Nat.Prime p)] :

torsionUnits p ≤ CommGroup.torsion ℤ_[p]ˣ

source

theorem PadicInt.card_torsionUnits (p : ℕ) [Fact (Nat.Prime p)] :

Nat.card ↥(torsionUnits p) = (p ^ torsionfreeUnitsExponent p).totient

source

@[simp]

theorem PadicInt.torsionfreeUnits_sup_torsionUnits (p : ℕ) [Fact (Nat.Prime p)] :

torsionfreeUnits p ⊔ torsionUnits p = ⊤

source

@[simp]

theorem PadicInt.disjoint_principalUnits_torsionUnits_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Disjoint (principalUnits p n) (torsionUnits p) ↔ torsionfreeUnitsExponent p ≤ n

source

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

Disjoint (torsionfreeUnits p) (torsionUnits p)

source

@[simp]

theorem PadicInt.cardinalMk_units_eq_continuum (p : ℕ) [Fact (Nat.Prime p)] :

Cardinal.mk ℤ_[p]ˣ = Cardinal.continuum

source

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 #

source

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

Instances For

source

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)

source

@[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 #

source

theorem PadicInt.isUnit_one_add_pow_torsionfreeUnitsExponent_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

IsUnit (1 + ↑p ^ torsionfreeUnitsExponent p)

source

theorem PadicInt.one_add_pow_torsionfreeUnitsExponent_toZModPow_mem_torsionfreeZModPowUnits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

⋯.unit ∈ torsionfreeZModPowUnits p n

source

@[simp]

theorem PadicInt.orderOf_one_add_pow_torsionfreeUnitsExponent_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

orderOf (1 + ↑p ^ torsionfreeUnitsExponent p) = p ^ n

source

theorem PadicInt.isOfFinOrder_one_add_pow_torsionfreeUnitsExponent_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

IsOfFinOrder (1 + ↑p ^ torsionfreeUnitsExponent p)

source

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, ⋯⟩

Instances For

source

@[simp]

theorem PadicInt.torsionfreeZModPowUnits.coe_generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

↑(generator p n) = ⋯.unit

source

@[simp]

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

orderOf (generator p n) = p ^ n

source

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

IsOfFinOrder (generator p n)

source

theorem PadicInt.torsionfreeZModPowUnits.zpowers_generator (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Subgroup.zpowers (generator p n) = ⊤

source

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

IsCyclic ↥(torsionfreeZModPowUnits p n)

source

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ⁿℤₚ, *) ≃ (ℤₚ, +)` #

source

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

((toZModPow i) x).val = x.appr i

source

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

source

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

source

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

Instances For

source

@[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

source

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_natCast (p : ℕ) [Fact (Nat.Prime p)] (x : ℕ) :

toFun p ↑x = (1 + ↑p ^ torsionfreeUnitsExponent p) ^ x

source

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_zero (p : ℕ) [Fact (Nat.Prime p)] :

toFun p 0 = 1

source

@[simp]

theorem PadicInt.equivTorsionfreeUnits.toFun_one (p : ℕ) [Fact (Nat.Prime p)] :

toFun p 1 = 1 + ↑p ^ torsionfreeUnitsExponent p

source

@[simp]

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

toFun p (x + y) = toFun p x * toFun p y

source

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

IsUnit (toFun p x)

source

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}

source

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

⋯.unit ∈ torsionfreeUnits p

source

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

Function.Injective (toFun p)

source

theorem PadicInt.equivTorsionfreeUnits.toFun_surjective (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(torsionfreeUnits p)) :

∃ (y : ℤ_[p]), toFun p y = ↑↑x

source

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