# Units of a number field #

We prove some basic results on the group (π K)Λ£ of units of the ring of integers π K of a number field K and its torsion subgroup.

## Main definition #

• NumberField.Units.torsion: the torsion subgroup of a number field.

## Main results #

• NumberField.isUnit_iff_norm: an algebraic integer x : π K is a unit if and only if |norm β x| = 1.

• NumberField.Units.mem_torsion: a unit x : (π K)Λ£ is torsion iff w x = 1 for all infinite places w of K.

## Tags #

number field, units

theorem Rat.RingOfIntegers.isUnit_iff :
β βx = 1 β¨ βx = -1
theorem NumberField.isUnit_iff_norm {K : Type u_1} [] [] {x : } :
β |β( x)| = 1
Equations
• = { coe := fun (x : ) => βx }
theorem NumberField.Units.coe_injective (K : Type u_1) [] :
Function.Injective fun (x : ) => βx
theorem NumberField.Units.coe_coe {K : Type u_1} [] (u : ) :
ββu = βu
theorem NumberField.Units.coe_mul {K : Type u_1} [] (x : ) (y : ) :
β(x * y) = βx * βy
theorem NumberField.Units.coe_pow {K : Type u_1} [] (x : ) (n : β) :
β(x ^ n) = βx ^ n
theorem NumberField.Units.coe_zpow {K : Type u_1} [] (x : ) (n : β€) :
β(x ^ n) = βx ^ n
theorem NumberField.Units.coe_one {K : Type u_1} [] :
β1 = 1
theorem NumberField.Units.coe_neg_one {K : Type u_1} [] :
β(-1) = -1
theorem NumberField.Units.coe_ne_zero {K : Type u_1} [] (x : ) :
βx β  0
@[simp]
theorem NumberField.Units.norm (K : Type u_1) [] [] (x : ) :
| ( βx)| = 1
def NumberField.Units.torsion (K : Type u_1) [] :

The torsion subgroup of the group of units.

Equations
Instances For
theorem NumberField.Units.mem_torsion (K : Type u_1) [] {x : } [] :
β β (w : ), w ( βx) = 1

The torsion subgroup is finite.

Equations

The torsion subgroup is cylic.

Equations
• β― = β―

The order of the torsion subgroup as a positive integer.

Equations
If k does not divide torsionOrder then there are no nontrivial roots of unity of order dividing k.
The group of roots of unity of order dividing torsionOrder is equal to the torsion group.