OAI/GroupTheory/PolycyclicRecognition/Algebra/WordExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.wordPrefix_congr line 10

   Source documentation

   Prefixes depend only on the increments preceding them.

   theorem wordPrefix_congr {A : Type*} [Monoid A] {u v : ℕ → A} (m : ℕ)
       (h : ∀ i < m, u i = v i) : wordPrefix u m = wordPrefix v m := by
   …

   Mentions: OAI.PolycyclicRecognition.wordPrefix

2. def OAI.PolycyclicRecognition.extendWord line 19

   Source documentation

   Append a prescribed increment, with irrelevant later increments fixed to it.

   def extendWord {A : Type*} (u : ℕ → A) (m : ℕ) (a : A) : ℕ → A :=
   …

3. theorem OAI.PolycyclicRecognition.extendWord_before line 22
4. theorem OAI.PolycyclicRecognition.extendWord_at line 25
5. theorem OAI.PolycyclicRecognition.wordPrefix_extendWord line 28
6. theorem OAI.PolycyclicRecognition.wordPrefix_extendWord_succ line 32