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 integerx : π K
is a unit if and only if|norm β x| = 1
.NumberField.Units.mem_torsion
: a unitx : (π K)Λ£
is torsion iffw x = 1
for all infinite placesw
ofK
.
Tags #
number field, units
theorem
NumberField.isUnit_iff_norm
{K : Type u_1}
[Field K]
[NumberField K]
{x : RingOfIntegers K}
:
@[simp]
theorem
NumberField.Units.norm
(K : Type u_1)
[Field K]
[NumberField K]
(x : (RingOfIntegers K)Λ£)
:
instance
NumberField.Units.instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion
(K : Type u_1)
[Field K]
[NumberField K]
:
The torsion subgroup is finite.
instance
NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion
(K : Type u_1)
[Field K]
[NumberField K]
:
The torsion subgroup is cyclic.
The order of the torsion subgroup as a positive integer.
Equations
Instances For
theorem
NumberField.Units.rootsOfUnity_eq_one
(K : Type u_1)
[Field K]
[NumberField K]
{k : β+}
(hc : (βk).Coprime β(torsionOrder K))
{ΞΆ : (RingOfIntegers K)Λ£}
:
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.