OAI/Combinatorics/Chromatic/Walls/LaurentCompletion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.BiSupported.neg line 23
  2. def OAI.ElementaryPositivity.QuantumTorus.biSupportedSubring line 31
  3. lemma OAI.ElementaryPositivity.QuantumTorus.biRegrade_zero line 38
  4. def OAI.ElementaryPositivity.QuantumTorus.biRegradeHom line 44
  5. def OAI.ElementaryPositivity.QuantumTorus.oldLaurent line 51
  6. def OAI.ElementaryPositivity.QuantumTorus.oldLaurentHom line 53
  7. lemma OAI.ElementaryPositivity.QuantumTorus.oldLaurent_mul line 55
  8. lemma OAI.ElementaryPositivity.QuantumTorus.oldLaurent_injective line 60
  9. lemma OAI.ElementaryPositivity.QuantumTorus.oldLaurent_read line 69
  10. def OAI.ElementaryPositivity.QuantumTorus.pureDegree line 78
  11. lemma OAI.ElementaryPositivity.QuantumTorus.completed_biSupported line 83
  12. lemma OAI.ElementaryPositivity.RationalFiber.expand_embed_coeff line 113
  13. lemma OAI.ElementaryPositivity.RationalFiber.hahn_power_negative line 132
  14. lemma OAI.ElementaryPositivity.RationalFiber.regrade_eval_vanish line 140
  15. lemma OAI.ElementaryPositivity.RationalFiber.regrade_expand_nat line 144
  16. lemma OAI.ElementaryPositivity.RationalFiber.rational_old_square line 177