OAI/Combinatorics/Chromatic/Walls/CompletedInverse.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.neg line 18
  2. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.mul line 23
  3. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.one line 34
  4. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.sub line 41
  5. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.pow line 45
  6. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.pow line 51
  7. lemma OAI.ElementaryPositivity.QuantumTorus.coeff_inverse_one line 61
  8. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.inverse line 69
  9. theorem OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.inverse line 88
  10. def OAI.ElementaryPositivity.QuantumTorus.completedInverse line 114
  11. lemma OAI.ElementaryPositivity.QuantumTorus.completedInverse_mul line 118
  12. lemma OAI.ElementaryPositivity.QuantumTorus.mul_completedInverse line 121
  13. def OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint line 134
  14. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.constant_adjoint line 135
  15. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.inverse_mul line 137
  16. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_mul line 147
  17. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.inverse_coeff_congr line 150
  18. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_coeff_congr line 164
  19. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.coeff_mul_vanish_right line 171
  20. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.coeff_mul_vanish_left line 186
  21. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_sub line 201
  22. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_leading line 203