OAI/Combinatorics/Chromatic/QuantumTorus/RationalPureAction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.gaugeMonomial line 14
  2. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.gaugeAdd line 18
  3. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.gaugeAdd_monomial line 20
  4. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.gaugeAdd_mul line 23
  5. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.gaugeAdd_one line 43
  6. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.gauge line 46
  7. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.gauge_monomial line 51
  8. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.gauge_comp line 55
  9. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.gaugeAdd_trivial line 64
  10. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_val_add line 73
  11. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_inv_val_add line 77
  12. def OAI.ElementaryPositivity.RationalFiber.pureActionHom line 81
  13. def OAI.ElementaryPositivity.RationalFiber.pureActionInvHom line 83
  14. lemma OAI.ElementaryPositivity.RationalFiber.pureAction_cancel line 85
  15. lemma OAI.ElementaryPositivity.RationalFiber.pureActionInv_cancel line 90
  16. def OAI.ElementaryPositivity.RationalFiber.pureAction line 95
  17. lemma OAI.ElementaryPositivity.RationalFiber.pureAction_monomial line 98
  18. lemma OAI.ElementaryPositivity.RationalFiber.pureAction_coefficient line 102
  19. def OAI.ElementaryPositivity.RationalFiber.completedPureAction line 106