OAI/MathematicalPhysics/Heisenberg/PhysicalClock.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Heisenberg.SlotTensor.SiteEdges line 12
  2. abbrev OAI.Heisenberg.SlotTensor.ClockEdges line 13
  3. def OAI.Heisenberg.SlotTensor.clockEdgeEquiv line 15
  4. def OAI.Heisenberg.SlotTensor.clockGenerator line 21
  5. def OAI.Heisenberg.SlotTensor.spinGenerator line 24
  6. lemma OAI.Heisenberg.SlotTensor.sum_clock_pair line 27
  7. lemma OAI.Heisenberg.SlotTensor.generator_intertwines line 35