OAI/Combinatorics/PolynomialVacuum/Algebra/Gram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumAlgebra.spin_zero_ne_plus line 7
  2. theorem OAI.PolynomialVacuumAlgebra.spin_zero_ne_minus line 8
  3. theorem OAI.PolynomialVacuumAlgebra.spin_plus_ne_zero line 9
  4. theorem OAI.PolynomialVacuumAlgebra.spin_plus_ne_minus line 10
  5. theorem OAI.PolynomialVacuumAlgebra.spin_minus_ne_zero line 11
  6. theorem OAI.PolynomialVacuumAlgebra.spin_minus_ne_plus line 12
  7. theorem OAI.PolynomialVacuumAlgebra.sum_spin line 14
  8. theorem OAI.PolynomialVacuumAlgebra.sum_pair line 21
  9. theorem OAI.PolynomialVacuumAlgebra.cup_zero_zero line 29
  10. theorem OAI.PolynomialVacuumAlgebra.cup_plus_minus line 30
  11. theorem OAI.PolynomialVacuumAlgebra.cup_minus_plus line 31
  12. theorem OAI.PolynomialVacuumAlgebra.cup_norm line 34
  13. theorem OAI.PolynomialVacuumAlgebra.cup_insertion_zero line 40
  14. theorem OAI.PolynomialVacuumAlgebra.cup_insertion line 47
  15. theorem OAI.PolynomialVacuumAlgebra.insertion_zero_norm line 53
  16. theorem OAI.PolynomialVacuumAlgebra.insertion_plus_norm line 58
  17. theorem OAI.PolynomialVacuumAlgebra.insertion_minus_norm line 65
  18. theorem OAI.PolynomialVacuumAlgebra.insertion_gram line 72