Conjugates of a unit in unit rank one #
In a number field of unit rank one, a unit whose value at a real infinite place exceeds 1 has
all its other conjugates of absolute value at most 1.
Main results #
TauCeti.NumberField.Units.norm_le_one_of_mem_roots_erase: the roots inℂof the minimal polynomial of such a unit, other than its value at that real place, have norm at most1.
theorem
TauCeti.NumberField.Units.norm_le_one_of_mem_roots_erase
{K : Type u_1}
[Field K]
[NumberField K]
(hr : NumberField.Units.rank K = 1)
{w : NumberField.InfinitePlace K}
(hw : w.IsReal)
(v : (NumberField.RingOfIntegers K)ˣ)
(hw1 : 1 < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑v))
{z : ℂ}
(hz :
z ∈ (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ ((algebraMap (NumberField.RingOfIntegers K) K) ↑v))).roots.erase
(w.embedding ((algebraMap (NumberField.RingOfIntegers K) K) ↑v)))
:
The conjugates of a unit of a number field of unit rank one, other than its value at a real
place where it exceeds 1, have absolute value at most 1.