OAI/Combinatorics/Chromatic/Walls/SimpleIncomingElement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.simpleRoot_ray_iff line 16
  2. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncoming_simple line 27
  3. lemma OAI.ElementaryPositivity.QuantumTorus.nonp_zero_of_simple_ray line 55
  4. lemma OAI.ElementaryPositivity.QuantumTorus.pureFaceSeries_eq_through line 62
  5. lemma OAI.ElementaryPositivity.QuantumTorus.pureFace_simpleTransport_value line 74
  6. lemma OAI.ElementaryPositivity.QuantumTorus.pure_simple_wall line 80
  7. lemma OAI.ElementaryPositivity.QuantumTorus.pure_joint_factor line 105
  8. def OAI.ElementaryPositivity.QuantumTorus.completedOne line 139
  9. def OAI.ElementaryPositivity.QuantumTorus.completedMul line 141
  10. def OAI.ElementaryPositivity.QuantumTorus.completedConjugate line 144
  11. lemma OAI.ElementaryPositivity.QuantumTorus.chartZero_right_negative line 146
  12. lemma OAI.ElementaryPositivity.QuantumTorus.chartZero_left_positive line 167