OAI/LinearAlgebra/CirculantHadamard/Kronecker.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Kronecker's criterion for the actual finite cyclotomic adjoin

Every embedding of the field generated by the chosen roots restricts to a unital ring homomorphism of their integral adjoin. This supplies the norm hypothesis in Kronecker's theorem. The field, its finite dimension, and the integrality of the selected element are constructed from the generators.

  1. theorem OAI.CirculantHadamard.root_of_unity_of_norm_embeddings line 21

    Source documentation

    An algebraic integer in a number field with all embedding norms equal to one is a root of unity, with a positive exponent.

    theorem root_of_unity_of_norm_embeddings (K : Type uK) [Field K] [NumberField K]
    {z : K} (hzi : IsIntegral ℤ z)
    (hz : ∀ σ : K →+* ℂ, ‖σ z‖ = 1) :
    ∃ n : ℕ, 0 < n ∧ z ^ n = 1 := by
…
  2. theorem OAI.CirculantHadamard.finite_adjoin_root_of_unity line 29