OAI/GroupTheory/PolycyclicRecognition/Algebra/PositiveAnnihilatorPropagation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Propagating a positive annihilator relation

A relation expressing the identity as a finite sum of strictly positive translates lets one push every translate into the nonnegative half-space. This is the elementary algebraic step in the monoid-ring criterion for a Bieri--Strebel direction.

  1. theorem OAI.PolycyclicRecognition.submodule_stable_of_positive_relation line 20