OAI/Combinatorics/Chromatic/Walls/LaurentPositiveDomination.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.nonneg line 10
  2. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.eq_zero_of_neg line 14
  3. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.eq_zero_of_sub line 20
  4. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.ne_zero_of_sub_one line 24
  5. def OAI.ElementaryPositivity.TriangularDynamics.triangularBase line 46
  6. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularBase_order line 47
  7. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularExpression_initial_graded line 49
  8. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularPower_incoming_retain line 56
  9. def OAI.ElementaryPositivity.TriangularDynamics.triangularConeTheta line 85
  10. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularConeTheta_positive line 89
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularPower_domination line 100
  12. lemma OAI.ElementaryPositivity.TriangularDynamics.adjoint_one_torus line 118
  13. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularTheta_support line 123
  14. lemma OAI.ElementaryPositivity.TriangularDynamics.pureAnchor_injective line 148
  15. lemma OAI.ElementaryPositivity.TriangularDynamics.stationary_pure_dominant line 154
  16. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularPureIncoming_dominant line 165
  17. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularPureIncoming_delta line 169