OAI/Combinatorics/PolynomialVacuum/Pairing/RowDuality.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.oppositeSpin line 8
  2. theorem OAI.PolynomialVacuumAlgebra.oppositeSpin_invol line 10
  3. theorem OAI.PolynomialVacuumAlgebra.charge_oppositeSpin line 11
  4. def OAI.PolynomialVacuumAlgebra.oppositeSpinEquiv line 12
  5. def OAI.PolynomialVacuumAlgebra.triangleUp line 13
  6. def OAI.PolynomialVacuumAlgebra.triangleDown line 14
  7. theorem OAI.PolynomialVacuumAlgebra.triangleUp_dual line 16
  8. theorem OAI.PolynomialVacuumAlgebra.triangleDown_dual line 20
  9. def OAI.PolynomialVacuumAlgebra.triangleRowWeight line 23
  10. theorem OAI.PolynomialVacuumAlgebra.finite_angle_product line 26
  11. theorem OAI.PolynomialVacuumAlgebra.row_triangle_weight line 36
  12. def OAI.PolynomialVacuumAlgebra.shiftForward line 45
  13. def OAI.PolynomialVacuumAlgebra.dualAux line 46
  14. def OAI.PolynomialVacuumAlgebra.dualInternal line 47
  15. theorem OAI.PolynomialVacuumAlgebra.triangleRowWeight_dual line 49
  16. theorem OAI.PolynomialVacuumAlgebra.triangleRowWeight_zero_ice line 58