OAI/GroupTheory/PolycyclicRecognition/Algebra/WordExponents.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Additive exponents of bracket words

Letter amplitudes add through every bracket. The sum in a word basis is the letter-count expression used by the support datum.

  1. def OAI.PolycyclicRecognition.bracketWordExponent line 17
  2. theorem OAI.PolycyclicRecognition.bracketWordExponent_of line 20
  3. theorem OAI.PolycyclicRecognition.bracketWordExponent_mul line 24
  4. theorem OAI.PolycyclicRecognition.sum_bracketWordExponent line 28
  5. theorem OAI.PolycyclicRecognition.bracketWordExponent_add line 34
  6. theorem OAI.PolycyclicRecognition.bracketWordExponent_const_mul line 39

    Source documentation

    Multiplying all letter costs multiplies every bracket-word cost.

    @[simp] theorem bracketWordExponent_const_mul (a : ℝ) (s : I → ℝ) (w : FreeMagma I) :
    bracketWordExponent (fun i => a * s i) w = a * bracketWordExponent s w := by
…

    Mentions: OAI.PolycyclicRecognition.bracketWordExponent