Units of a number field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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

source

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

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

source

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