OAI/GroupTheory/PolycyclicRecognition/Algebra/NumberFieldExpandingPlace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An expanding place for a nontorsion algebraic number

If all finite-place norms are at most one, the element is an algebraic integer. Kronecker's theorem then supplies an expanding complex embedding unless the element is a root of unity.

  1. theorem OAI.PolycyclicRecognition.nonintegral_has_expanding_finite_place line 17
  2. theorem OAI.PolycyclicRecognition.nontorsion_numberField_expanding_place line 34
  3. theorem OAI.PolycyclicRecognition.nontorsion_numberField_expanding_absoluteValue line 43