OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteAlgebraIndependentBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A generator bound for independent coordinates in a finite algebra

The algebra may have zero divisors. Passing to a prime quotient that preserves the chosen independent coordinates reduces the bound to the domain case.

  1. theorem OAI.PolycyclicRecognition.algebraicIndependent_card_le_of_finite_adjoin line 18