OAI/Combinatorics/PolynomialVacuum/Algebra/SpectatorFiltration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumAlgebra.spectatorSlot line 8
2. theorem OAI.PolynomialVacuumAlgebra.spectatorSlot_last line 11
3. theorem OAI.PolynomialVacuumAlgebra.spectatorSlot_self_left line 13
4. theorem OAI.PolynomialVacuumAlgebra.spectatorSlot_self_right line 15
5. theorem OAI.PolynomialVacuumAlgebra.spectatorSlot_other line 18
6. theorem OAI.PolynomialVacuumAlgebra.tensorExchange_spectator_filtration line 40
7. theorem OAI.PolynomialVacuumAlgebra.tensorExchange_unaffected_filtration line 58
8. theorem OAI.PolynomialVacuumAlgebra.transportCup_spectator_filtration line 74