OAI/Combinatorics/PolynomialVacuum/Algebra/Projectors.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.insertionMatrix line 7
  2. def OAI.PolynomialVacuumAlgebra.cupColumn line 9
  3. theorem OAI.PolynomialVacuumAlgebra.cupColumn_gram line 11
  4. theorem OAI.PolynomialVacuumAlgebra.insertion_matrix_gram line 16
  5. theorem OAI.PolynomialVacuumAlgebra.cupColumn_insertion line 22
  6. theorem OAI.PolynomialVacuumAlgebra.insertion_cupColumn line 28
  7. theorem OAI.PolynomialVacuumAlgebra.Pzero_factor line 32
  8. theorem OAI.PolynomialVacuumAlgebra.Pone_factor line 37
  9. theorem OAI.PolynomialVacuumAlgebra.gram_projection_idempotent line 43
  10. theorem OAI.PolynomialVacuumAlgebra.gram_projection_orthogonal line 53
  11. theorem OAI.PolynomialVacuumAlgebra.Pzero_idempotent line 61
  12. theorem OAI.PolynomialVacuumAlgebra.Pone_idempotent line 65
  13. theorem OAI.PolynomialVacuumAlgebra.Pzero_Pone line 69
  14. theorem OAI.PolynomialVacuumAlgebra.Pone_Pzero line 73
  15. theorem OAI.PolynomialVacuumAlgebra.Pzero_Ptwo line 77
  16. theorem OAI.PolynomialVacuumAlgebra.Ptwo_Pzero line 80
  17. theorem OAI.PolynomialVacuumAlgebra.Pone_Ptwo line 83
  18. theorem OAI.PolynomialVacuumAlgebra.Ptwo_Pone line 86
  19. theorem OAI.PolynomialVacuumAlgebra.Ptwo_idempotent line 89
  20. theorem OAI.PolynomialVacuumAlgebra.projectors_sum line 94