OAI/Analysis/FreeWords/TransportBlocks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KKFiniteTransport.Block line 22
  2. def OAI.KKFiniteTransport.blockValue line 26
  3. def OAI.KKFiniteTransport.blockCenter line 29
  4. def OAI.KKFiniteTransport.conjStarMonoid line 32
  5. def OAI.KKFiniteTransport.conjUnitary line 36
  6. theorem OAI.KKFiniteTransport.conjUnitary_val line 39
  7. theorem OAI.KKFiniteTransport.conjUnitary_zpow line 42
  8. theorem OAI.KKFiniteTransport.conjUnitary_good line 48
  9. theorem OAI.KKFiniteTransport.powerWord_conj line 55
  10. theorem OAI.KKFiniteTransport.blockValue_conj line 71
  11. theorem OAI.KKFiniteTransport.blockCenter_conj line 77