OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteTypeExpandingEmbedding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A valued embedding that expands a specified nontorsion element

The coefficient field may have finite transcendence degree. For an algebraic element, choose a place of its number field and extend that embedding. For a transcendental element, use an expanding complex specialization.

  1. theorem OAI.PolycyclicRecognition.numberField_expanding_normed_embedding line 18
  2. theorem OAI.PolycyclicRecognition.finiteType_nontorsion_expanding_embedding line 39