Documentation

Mathlib.NumberTheory.NumberField.Units.Basic

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 #

Main results #

Tags #

number field, units

theorem NumberField.Units.coe_mul {K : Type u_1} [Field K] (x y : (RingOfIntegers K)Λ£) :
(algebraMap (RingOfIntegers K) K) ↑(x * y) = (algebraMap (RingOfIntegers K) K) ↑x * (algebraMap (RingOfIntegers K) K) ↑y
theorem NumberField.Units.coe_pow {K : Type u_1} [Field K] (x : (RingOfIntegers K)Λ£) (n : β„•) :
(algebraMap (RingOfIntegers K) K) ↑(x ^ n) = (algebraMap (RingOfIntegers K) K) ↑x ^ n
theorem NumberField.Units.coe_zpow {K : Type u_1} [Field K] (x : (RingOfIntegers K)Λ£) (n : β„€) :
(algebraMap (RingOfIntegers K) K) ↑(x ^ n) = (algebraMap (RingOfIntegers K) K) ↑x ^ n
theorem NumberField.Units.coe_one {K : Type u_1} [Field K] :
(algebraMap (RingOfIntegers K) K) ↑1 = 1
theorem NumberField.Units.coe_neg_one {K : Type u_1} [Field K] :
(algebraMap (RingOfIntegers K) K) ↑(-1) = -1
@[simp]

The order of the torsion subgroup as a positive integer.

Equations

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.