mathlib documentation

number_theory.number_field.units

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 integer x : 𝓞 K is a unit if and only if |norm ℚ x| = 1

Tags #

number field, units

theorem rat.ring_of_integers.is_unit_iff {x : ↥(number_field.ring_of_integers ℚ)} :

is_unit x ↔ ↑x = 1 ∨ ↑x = -1

theorem is_unit_iff_norm {K : Type u_1} [field K] [number_field K] (x : ↥(number_field.ring_of_integers K)) :

is_unit x ↔ |↑(⇑(ring_of_integers.norm ℚ) x)| = 1