OAI/GroupTheory/PolycyclicRecognition/Algebra/AlgebraicIndependentPrimeQuotient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Preserve independent polynomial coordinates in a domain quotient

This is the domain reduction needed when a commutative algebra of operators has zero divisors. A prime disjoint from the nonzero polynomial coordinates preserves their algebraic independence.

  1. theorem OAI.PolycyclicRecognition.algebraicIndependent_prime_quotient line 19