Algebraic integer conjugate norm bound

Stream: Is there code for X?

[Michail Karatarakis]

Do we have this?

Let $\alpha$ be a non-zero algebraic integer. Then $\alpha$ has a conjugate $\alpha^{(i)}$ with $\lvert \alpha^{(i)} \rvert \geq 1$.

[Riccardo Brasca]

I don't think we have this precise statement, but it should easy to prove: the absolute value of the norm is a least 1, so it's not possible that all the conjugate have absolute value less than 1.

[Riccardo Brasca]

Note that we have NumberField.Embeddings.pow_eq_one_of_norm_eq_one, so we know that, except in the root of unity case, there is a conjugate with absolute value strictly bigger than 1.

[Xavier Roblot]

The result should be easy to prove using docs#NumberField.InfinitePlace.one_le_of_lt_one