OAI/GroupTheory/PolycyclicRecognition/Algebra/FilteredNilpotentPerturbation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent perturbations along a finite filtration

An operator which agrees with a nilpotent operator on each successive quotient is nilpotent. No commutation of the two operators is required.

  1. theorem OAI.PolycyclicRecognition.nilpotent_of_raises_finite_filtration line 18
  2. theorem OAI.PolycyclicRecognition.nilpotent_of_filtered_nilpotent_perturbation line 31