OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteTraceLinearGroup.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finiteness from finitely many traces in a full matrix span

A finite spanning subset of the group supplies trace coordinates. The trace pairing is nondegenerate, so these coordinates separate group elements. This is the concrete finite-trace step used in Tits, Section 2.

  1. theorem OAI.PolycyclicRecognition.finite_matrix_group_of_full_span_finite_trace line 17