# Documentation

This file defines the p-adic integers ℤ_[p] as the subtype of ℚ_[p] with norm ≤ 1. We show that ℤ_[p]

• is complete,
• is nonarchimedean,
• is a normed ring,
• is a local ring, and
• is a discrete valuation ring.

The relation between ℤ_[p] and ZMod p is established in another file.

## Important definitions #

• PadicInt : the type of p-adic integers

## Notation #

We introduce the notation ℤ_[p] for the p-adic integers.

## Implementation notes #

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking [Fact p.Prime] as a type class argument.

Coercions into ℤ_[p] are set up to work with the norm_cast tactic.

## Tags #

def PadicInt (p : ) [Fact ()] :

The p-adic integers ℤ_[p] are the p-adic numbers with norm ≤ 1.

Equations
Instances For

The ring of p-adic integers.

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

### Ring structure and coercion to ℚ_[p]#

Equations
theorem PadicInt.ext {p : } [Fact ()] {x : ℤ_[p]} {y : ℤ_[p]} :
x = yx = y
def PadicInt.subring (p : ) [Fact ()] :

The p-adic integers as a subring of ℚ_[p].

Equations
• = { carrier := {x : ℚ_[p] | x 1}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , neg_mem' := }
Instances For
@[simp]
theorem PadicInt.mem_subring_iff (p : ) [Fact ()] {x : ℚ_[p]} :

Addition on ℤ_[p] is inherited from ℚ_[p].

Equations
instance PadicInt.instMul {p : } [Fact ()] :

Multiplication on ℤ_[p] is inherited from ℚ_[p].

Equations
instance PadicInt.instNeg {p : } [Fact ()] :

Negation on ℤ_[p] is inherited from ℚ_[p].

Equations
instance PadicInt.instSub {p : } [Fact ()] :

Subtraction on ℤ_[p] is inherited from ℚ_[p].

Equations
instance PadicInt.instZero {p : } [Fact ()] :

Zero on ℤ_[p] is inherited from ℚ_[p].

Equations
instance PadicInt.instInhabited {p : } [Fact ()] :
Equations
• PadicInt.instInhabited = { default := 0 }
instance PadicInt.instOne {p : } [Fact ()] :

One on ℤ_[p] is inherited from ℚ_[p].

Equations
• PadicInt.instOne = { one := 1, }
@[simp]
theorem PadicInt.mk_zero {p : } [Fact ()] {h : 0 1} :
0, h = 0
@[simp]
theorem PadicInt.coe_add {p : } [Fact ()] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
(z1 + z2) = z1 + z2
@[simp]
theorem PadicInt.coe_mul {p : } [Fact ()] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
(z1 * z2) = z1 * z2
@[simp]
theorem PadicInt.coe_neg {p : } [Fact ()] (z1 : ℤ_[p]) :
(-z1) = -z1
@[simp]
theorem PadicInt.coe_sub {p : } [Fact ()] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
(z1 - z2) = z1 - z2
@[simp]
theorem PadicInt.coe_one {p : } [Fact ()] :
1 = 1
@[simp]
theorem PadicInt.coe_zero {p : } [Fact ()] :
0 = 0
theorem PadicInt.coe_eq_zero {p : } [Fact ()] (z : ℤ_[p]) :
z = 0 z = 0
theorem PadicInt.coe_ne_zero {p : } [Fact ()] (z : ℤ_[p]) :
z 0 z 0
Equations
instance PadicInt.instCommRing {p : } [Fact ()] :
Equations
@[simp]
theorem PadicInt.coe_natCast {p : } [Fact ()] (n : ) :
n = n
theorem PadicInt.coe_nat_cast {p : } [Fact ()] (n : ) :
n = n

Alias of PadicInt.coe_natCast.

@[simp]
theorem PadicInt.coe_intCast {p : } [Fact ()] (z : ) :
z = z
theorem PadicInt.coe_int_cast {p : } [Fact ()] (z : ) :
z = z

Alias of PadicInt.coe_intCast.

def PadicInt.Coe.ringHom {p : } [Fact ()] :

The coercion from ℤ_[p] to ℚ_[p] as a ring homomorphism.

Equations
Instances For
@[simp]
theorem PadicInt.coe_pow {p : } [Fact ()] (x : ℤ_[p]) (n : ) :
(x ^ n) = x ^ n
theorem PadicInt.mk_coe {p : } [Fact ()] (k : ℤ_[p]) :
k, = k
def PadicInt.inv {p : } [Fact ()] :

The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the inverse is defined to be 0.

Equations
• x.inv = match x with | k, property => if h : k = 1 then k⁻¹, else 0
Instances For
instance PadicInt.instCharZero {p : } [Fact ()] :
Equations
• =
theorem PadicInt.intCast_eq {p : } [Fact ()] (z1 : ) (z2 : ) :
z1 = z2 z1 = z2
theorem PadicInt.coe_int_eq {p : } [Fact ()] (z1 : ) (z2 : ) :
z1 = z2 z1 = z2

Alias of PadicInt.intCast_eq.

def PadicInt.ofIntSeq {p : } [Fact ()] (seq : ) (h : IsCauSeq () fun (n : ) => (seq n)) :

A sequence of integers that is Cauchy with respect to the p-adic norm converges to a p-adic integer.

Equations
• = fun (n : ) => (seq n), h,
Instances For

### Instances #

We now show that ℤ_[p] is a

• complete metric space
• normed ring
• integral domain
instance PadicInt.instMetricSpace (p : ) [Fact ()] :
Equations
• = Subtype.metricSpace
instance PadicInt.completeSpace (p : ) [Fact ()] :
Equations
• =
instance PadicInt.instNorm (p : ) [Fact ()] :
Equations
theorem PadicInt.norm_def {p : } [Fact ()] {z : ℤ_[p]} :
instance PadicInt.instNormedCommRing (p : ) [Fact ()] :
Equations
• = let __src := PadicInt.instCommRing;
instance PadicInt.instNormOneClass (p : ) [Fact ()] :
Equations
• =
instance PadicInt.isAbsoluteValue (p : ) [Fact ()] :
Equations
• =
instance PadicInt.instIsDomain {p : } [Fact ()] :
Equations
• =

### Norm #

theorem PadicInt.norm_le_one {p : } [Fact ()] (z : ℤ_[p]) :
@[simp]
theorem PadicInt.norm_mul {p : } [Fact ()] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
z1 * z2 = z1 * z2
@[simp]
theorem PadicInt.norm_pow {p : } [Fact ()] (z : ℤ_[p]) (n : ) :
z ^ n = z ^ n
theorem PadicInt.nonarchimedean {p : } [Fact ()] (q : ℤ_[p]) (r : ℤ_[p]) :
theorem PadicInt.norm_eq_of_norm_add_lt_right {p : } [Fact ()] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (h : z1 + z2 < z2) :
theorem PadicInt.norm_eq_of_norm_add_lt_left {p : } [Fact ()] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (h : z1 + z2 < z1) :
@[simp]
z = z

Alias of PadicInt.norm_intCast_eq_padic_norm.

@[simp]
theorem PadicInt.norm_eq_padic_norm {p : } [Fact ()] {q : ℚ_[p]} (hq : q 1) :
q, hq = q
@[simp]
theorem PadicInt.norm_p {p : } [Fact ()] :
p = (p)⁻¹
theorem PadicInt.norm_p_pow {p : } [Fact ()] (n : ) :
p ^ n = p ^ (-n)
instance PadicInt.complete (p : ) [Fact ()] :
Equations
• =
theorem PadicInt.exists_pow_neg_lt (p : ) [hp : Fact ()] {ε : } (hε : 0 < ε) :
∃ (k : ), p ^ (-k) < ε
theorem PadicInt.exists_pow_neg_lt_rat (p : ) [hp : Fact ()] {ε : } (hε : 0 < ε) :
∃ (k : ), p ^ (-k) < ε
theorem PadicInt.norm_int_lt_one_iff_dvd {p : } [hp : Fact ()] (k : ) :
k < 1 p k
theorem PadicInt.norm_int_le_pow_iff_dvd {p : } [hp : Fact ()] {k : } {n : } :
k p ^ (-n) p ^ n k

### Valuation on ℤ_[p]#

def PadicInt.valuation {p : } [hp : Fact ()] (x : ℤ_[p]) :

PadicInt.valuation lifts the p-adic valuation on ℚ to ℤ_[p].

Equations
• x.valuation = (x).valuation
Instances For
theorem PadicInt.norm_eq_pow_val {p : } [hp : Fact ()] {x : ℤ_[p]} (hx : x 0) :
x = p ^ (-x.valuation)
@[simp]
theorem PadicInt.valuation_zero {p : } [hp : Fact ()] :
@[simp]
theorem PadicInt.valuation_one {p : } [hp : Fact ()] :
@[simp]
theorem PadicInt.valuation_p {p : } [hp : Fact ()] :
(p).valuation = 1
theorem PadicInt.valuation_nonneg {p : } [hp : Fact ()] (x : ℤ_[p]) :
0 x.valuation
@[simp]
theorem PadicInt.valuation_p_pow_mul {p : } [hp : Fact ()] (n : ) (c : ℤ_[p]) (hc : c 0) :
(p ^ n * c).valuation = n + c.valuation

### Units of ℤ_[p]#

theorem PadicInt.mul_inv {p : } [hp : Fact ()] {z : ℤ_[p]} :
z = 1z * z.inv = 1
theorem PadicInt.inv_mul {p : } [hp : Fact ()] {z : ℤ_[p]} (hz : z = 1) :
z.inv * z = 1
theorem PadicInt.isUnit_iff {p : } [hp : Fact ()] {z : ℤ_[p]} :
theorem PadicInt.norm_lt_one_add {p : } [hp : Fact ()] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (hz1 : z1 < 1) (hz2 : z2 < 1) :
z1 + z2 < 1
theorem PadicInt.norm_lt_one_mul {p : } [hp : Fact ()] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (hz2 : z2 < 1) :
z1 * z2 < 1
theorem PadicInt.mem_nonunits {p : } [hp : Fact ()] {z : ℤ_[p]} :
def PadicInt.mkUnits {p : } [hp : Fact ()] {u : ℚ_[p]} (h : u = 1) :

A p-adic number u with ‖u‖ = 1 is a unit of ℤ_[p].

Equations
• = let z := u, ; { val := z, inv := z.inv, val_inv := , inv_val := }
Instances For
@[simp]
theorem PadicInt.mkUnits_eq {p : } [hp : Fact ()] {u : ℚ_[p]} (h : u = 1) :
() = u
@[simp]
theorem PadicInt.norm_units {p : } [hp : Fact ()] (u : ) :
u = 1
def PadicInt.unitCoeff {p : } [hp : Fact ()] {x : ℤ_[p]} (hx : x 0) :

unitCoeff hx is the unit u in the unique representation x = u * p ^ n. See unitCoeff_spec.

Equations
• = let u := x * p ^ (-x.valuation); let_fun hu := ;
Instances For
@[simp]
theorem PadicInt.unitCoeff_coe {p : } [hp : Fact ()] {x : ℤ_[p]} (hx : x 0) :
() = x * p ^ (-x.valuation)
theorem PadicInt.unitCoeff_spec {p : } [hp : Fact ()] {x : ℤ_[p]} (hx : x 0) :
x = () * p ^ x.valuation.natAbs

### Various characterizations of open unit balls #

theorem PadicInt.norm_le_pow_iff_le_valuation {p : } [hp : Fact ()] (x : ℤ_[p]) (hx : x 0) (n : ) :
x p ^ (-n) n x.valuation
theorem PadicInt.mem_span_pow_iff_le_valuation {p : } [hp : Fact ()] (x : ℤ_[p]) (hx : x 0) (n : ) :
x Ideal.span {p ^ n} n x.valuation
theorem PadicInt.norm_le_pow_iff_mem_span_pow {p : } [hp : Fact ()] (x : ℤ_[p]) (n : ) :
x p ^ (-n) x Ideal.span {p ^ n}
theorem PadicInt.norm_le_pow_iff_norm_lt_pow_add_one {p : } [hp : Fact ()] (x : ℤ_[p]) (n : ) :
x p ^ n x < p ^ (n + 1)
theorem PadicInt.norm_lt_pow_iff_norm_le_pow_sub_one {p : } [hp : Fact ()] (x : ℤ_[p]) (n : ) :
x < p ^ n x p ^ (n - 1)
theorem PadicInt.norm_lt_one_iff_dvd {p : } [hp : Fact ()] (x : ℤ_[p]) :
x < 1 p x
@[simp]
theorem PadicInt.pow_p_dvd_int_iff {p : } [hp : Fact ()] (n : ) (a : ) :
p ^ n a p ^ n a

### Discrete valuation ring #

instance PadicInt.instLocalRing {p : } [hp : Fact ()] :
Equations
• =
theorem PadicInt.p_nonnunit {p : } [hp : Fact ()] :
p
theorem PadicInt.prime_p {p : } [hp : Fact ()] :
Prime p
theorem PadicInt.irreducible_p {p : } [hp : Fact ()] :
instance PadicInt.instDiscreteValuationRing {p : } [hp : Fact ()] :
Equations
• =
theorem PadicInt.ideal_eq_span_pow_p {p : } [hp : Fact ()] {s : } (hs : s ) :
∃ (n : ), s = Ideal.span {p ^ n}
Equations
• =
instance PadicInt.algebra {p : } [hp : Fact ()] :
Equations