OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorOverlap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Comparing nonunique factor lifts

The error between two lifts is an actual element of the overlap of the two factor images. No centrality or discreteness of the overlap is used.

  1. theorem OAI.PolycyclicRecognition.factor_overlap_difference line 14