OAI/Combinatorics/Chromatic/Walls/PureActualCoefficients.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.actualMonomialAdjointCoefficient_read line 20
  2. lemma OAI.ElementaryPositivity.QuantumTorus.normalizedSimple_adjoint_coefficient line 31
  3. lemma OAI.ElementaryPositivity.QuantumTorus.actual_pure_monomial line 39
  4. def OAI.ElementaryPositivity.PowerSeriesAdjoint.hahnAction line 76
  5. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.hahnAction_add line 78
  6. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.hahnAction_zero line 81
  7. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.hahnAction_one line 83
  8. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.hahnAction_mul line 86
  9. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.hahnAction_inverse_cancel line 90
  10. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.ofPowerSeries_coeff_int line 93
  11. lemma OAI.ElementaryPositivity.QuantumTorus.adjoint_scalar_monomial_coeff line 115
  12. lemma OAI.ElementaryPositivity.QuantumTorus.hahnAction_monomial_coeff line 123
  13. lemma OAI.ElementaryPositivity.QuantumTorus.hahnAction_actual_coeff line 134
  14. lemma OAI.ElementaryPositivity.QuantumTorus.adjoint_monomial_degree line 152
  15. lemma OAI.ElementaryPositivity.QuantumTorus.hahnAction_diagonal line 167
  16. lemma OAI.ElementaryPositivity.QuantumTorus.hahnAction_finite_iff line 190