Units of a number field #
We prove results about the group
(𝓞 K)ˣ of units of the ring of integers
𝓞 K of a number
Main results #
isUnit_iff_norm: an algebraic integer
x : 𝓞 Kis a unit if and only if
|norm ℚ x| = 1.
mem_torsion: a unit
x : (𝓞 K)ˣis torsion iff
w x = 1for all infinite places of
number field, units
Shortcut instance because Lean tends to time out before finding the general instance.
The torsion subgroup is finite.
The torsion subgroup is cylic.
k does not divide
torsionOrder then there are no nontrivial roots of unity of
The group of roots of unity of order dividing
torsionOrder is equal to the torsion