OAI/Combinatorics/Chromatic/Walls/RealLatticeRealization.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.LatticeRealization.cast line 12
  2. lemma OAI.ElementaryPositivity.LatticeRealization.cast_apply line 18
  3. lemma OAI.ElementaryPositivity.LatticeRealization.cast_injective line 20
  4. def OAI.ElementaryPositivity.LatticeRealization.realPairing line 28
  5. lemma OAI.ElementaryPositivity.LatticeRealization.realPairing_apply line 31
  6. lemma OAI.ElementaryPositivity.LatticeRealization.realPairing_cast line 34
  7. lemma OAI.ElementaryPositivity.LatticeRealization.realPairing_skew line 38
  8. lemma OAI.ElementaryPositivity.LatticeRealization.realPairing_self line 49
  9. def OAI.ElementaryPositivity.LatticeRealization.realDot line 54
  10. lemma OAI.ElementaryPositivity.LatticeRealization.realDot_apply line 56
  11. lemma OAI.ElementaryPositivity.LatticeRealization.realDot_comm line 58
  12. lemma OAI.ElementaryPositivity.LatticeRealization.realDot_cast line 63
  13. def OAI.ElementaryPositivity.LatticeRealization.extendedCast line 67
  14. lemma OAI.ElementaryPositivity.LatticeRealization.extendedCast_apply line 70
  15. lemma OAI.ElementaryPositivity.LatticeRealization.extendedCast_injective line 73
  16. def OAI.ElementaryPositivity.LatticeRealization.extendedRealForm line 79
  17. lemma OAI.ElementaryPositivity.LatticeRealization.extendedRealForm_apply line 85
  18. lemma OAI.ElementaryPositivity.LatticeRealization.extendedRealForm_self line 88
  19. lemma OAI.ElementaryPositivity.LatticeRealization.extendedRealForm_cast line 92
  20. lemma OAI.ElementaryPositivity.ForwardChain.gaps_map line 104
  21. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardInventory_map line 113
  22. lemma OAI.ElementaryPositivity.TriangularDynamics.cast_single line 130
  23. lemma OAI.ElementaryPositivity.TriangularDynamics.cast_forwardGap line 135
  24. def OAI.ElementaryPositivity.TriangularDynamics.extendedRoots line 139
  25. def OAI.ElementaryPositivity.TriangularDynamics.extendedCoord line 142
  26. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedCoord_roots line 145
  27. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedRoot_eq line 147
  28. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedRoots_realIndependent line 150
  29. def OAI.ElementaryPositivity.TriangularDynamics.initialFreeChart line 166
  30. lemma OAI.ElementaryPositivity.TriangularDynamics.initialFreeChart_inventory line 172
  31. def OAI.ElementaryPositivity.TriangularDynamics.extendedOmega line 181
  32. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedOmega_self line 182
  33. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedOmega_nondegenerate line 183
  34. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedOmega_original line 184
  35. def OAI.ElementaryPositivity.TriangularDynamics.triangularRealForm line 186
  36. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularRealForm_self line 187
  37. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularRealForm_compatible line 189