OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteExponentSubquotients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-exponent actions are detected on an invariant subspace and quotient

An element acting trivially on both pieces differs from the identity by a square-zero operator. In characteristic zero a positive finite power can then be the identity only if the element itself is the identity.

  1. theorem OAI.PolycyclicRecognition.linear_eq_one_of_finite_power_trivial_subquotient line 19
  2. theorem OAI.PolycyclicRecognition.subquotient_action_pair_injective_of_finite_exponent line 43