OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteAlgebraicConstants.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Algebraic constants in a finitely generated field form a finite extension

After choosing a transcendence basis, a finite extension of its rational function field bounds every independent family of algebraic constants.

  1. theorem OAI.PolycyclicRecognition.algebraic_constants_rank_le line 16
  2. theorem OAI.PolycyclicRecognition.finite_algebraic_constants_of_transcendental_finite_extension line 28
  3. theorem OAI.PolycyclicRecognition.finite_algebraicClosure_of_essFiniteType line 37