OAI/Combinatorics/PolynomialVacuum/Algebra/TraceClosing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumAlgebra.padCup line 8
2. theorem OAI.PolynomialVacuumAlgebra.padCup_left line 9
3. theorem OAI.PolynomialVacuumAlgebra.padCup_right line 10
4. theorem OAI.PolynomialVacuumAlgebra.padCup_skip line 11
5. theorem OAI.PolynomialVacuumAlgebra.rotate_padCup_head line 16
6. theorem OAI.PolynomialVacuumAlgebra.rotate_padCup_tail line 20
7. theorem OAI.PolynomialVacuumAlgebra.numerator_cup_zero line 29
8. theorem OAI.PolynomialVacuumAlgebra.cup_trace_identity line 36
9. theorem OAI.PolynomialVacuumAlgebra.cupRow_trace line 45