OAI/Combinatorics/PolynomialVacuum/Algebra/TensorActions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialVacuumAlgebra.SpinTensor line 11
  2. def OAI.PolynomialVacuumAlgebra.replacePair line 13
  3. theorem OAI.PolynomialVacuumAlgebra.replacePair_left line 16
  4. theorem OAI.PolynomialVacuumAlgebra.replacePair_right line 18
  5. theorem OAI.PolynomialVacuumAlgebra.replacePair_other line 20
  6. theorem OAI.PolynomialVacuumAlgebra.replacePair_replacePair line 22
  7. def OAI.PolynomialVacuumAlgebra.pairAction line 31
  8. theorem OAI.PolynomialVacuumAlgebra.pairAction_mul line 34
  9. theorem OAI.PolynomialVacuumAlgebra.pairAction_smul line 46
  10. theorem OAI.PolynomialVacuumAlgebra.pairAction_scalar line 51
  11. theorem OAI.PolynomialVacuumAlgebra.replacePair_self line 59
  12. theorem OAI.PolynomialVacuumAlgebra.pairAction_one line 62
  13. theorem OAI.PolynomialVacuumAlgebra.replacePair_comm line 66
  14. theorem OAI.PolynomialVacuumAlgebra.pairAction_comm line 80