OAI/GroupTheory/PolycyclicRecognition/Algebra/IndependentAlgebraicConstants.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Algebraic constants stay independent over a transcendental field

Polynomial relations are compared coefficient by coefficient. Passing from the polynomial algebra to its fraction field then preserves independence.

  1. theorem OAI.PolycyclicRecognition.constants_linearIndependent_over_polynomial_algebra line 17
  2. theorem OAI.PolycyclicRecognition.algebraic_constants_linearIndependent_over_transcendental_field line 57