Theorems · Theorem · number theory

NumberField.Embeddings.pow_eq_one_of_norm_le_one

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

Kronecker's Theorem: A non-zero algebraic integer whose conjugates are all inside the closed unit disk is a root of unity.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldNormedFieldIsAlgClosedNormedAlgebra