Theorems · Theorem · number theory

NumberField.Embeddings.pow_eq_one_of_norm_eq_one

∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] {x : K}, IsIntegral ℤ x → (∀ (φ : K →+* A), ‖φ x‖ = 1) → ∃ n, ∃ (_ : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

1 results in Mathlib

Foundations

Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldNormedFieldIsAlgClosedNormedAlgebra