OAI/GroupTheory/PolycyclicRecognition/Algebra/IrreducibleFiniteTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An irreducible matrix group with finitely many traces is finite

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.irreducible_entries_span_eq_top line 14
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.finite_of_irreducible_finite_trace line 43