OAI/GroupTheory/PolycyclicRecognition/Algebra/AlgebraicExpandingEmbedding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An expanding complex embedding of a nontorsion algebraic integer

This is the integral number-field case of the norm-changing step. General finitely generated coefficient fields and nonintegral elements remain separate obligations.

  1. theorem OAI.PolycyclicRecognition.integral_nontorsion_has_expanding_complex_embedding line 15