Units of a number field #
We prove results about the group (𝓞 K)ˣ
of units of the ring of integers 𝓞 K
of a number
field K
.
Main results #
number_field.is_unit_iff_norm
: an algebraic integerx : 𝓞 K
is a unit if and only if|norm ℚ x| = 1
Tags #
number field, units
theorem
is_unit_iff_norm
{K : Type u_1}
[field K]
[number_field K]
(x : ↥(number_field.ring_of_integers K)) :