OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentDeshear.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.Deshear.single_central line 11
  2. lemma OAI.ElementaryPositivity.Deshear.shift_mul line 16
  3. def OAI.ElementaryPositivity.Deshear.deshear line 25
  4. lemma OAI.ElementaryPositivity.Deshear.deshear_coeff line 27
  5. lemma OAI.ElementaryPositivity.Deshear.deshear_read line 30
  6. lemma OAI.ElementaryPositivity.Deshear.deshear_zero line 36
  7. lemma OAI.ElementaryPositivity.Deshear.deshear_one line 40
  8. lemma OAI.ElementaryPositivity.Deshear.deshear_add line 48
  9. lemma OAI.ElementaryPositivity.Deshear.deshear_mul line 53
  10. def OAI.ElementaryPositivity.Deshear.deshearHom line 66
  11. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.bi_shear line 89
  12. lemma OAI.ElementaryPositivity.QuantumTorus.laurentHomogenize_shear_coeff line 96
  13. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_eq_deshear line 115
  14. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_mul line 145
  15. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_add line 152
  16. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_zero line 158
  17. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_one line 160
  18. def OAI.ElementaryPositivity.QuantumTorus.laurentBoundedSubring line 163
  19. def OAI.ElementaryPositivity.QuantumTorus.laurentRegradeHom line 171