OAI/GroupTheory/PolycyclicRecognition/Algebra/ComplexBinaryWords.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Separated binary words in a complex base

For a base of modulus at least two, distinct binary strings of the same length evaluate at distance at least one. This is the counting ingredient for excluding expanding characters of conjugation.

  1. def OAI.PolycyclicRecognition.complexBit line 16
  2. def OAI.PolycyclicRecognition.complexBinaryWord line 18
  3. theorem OAI.PolycyclicRecognition.complexBit_dist_le line 22
  4. theorem OAI.PolycyclicRecognition.complexBinaryWord_separated line 25
  5. theorem OAI.PolycyclicRecognition.complexBinaryWord_injective_length line 57