OAI/Combinatorics/PolynomialVacuum/Algebra/TransportFiltration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumAlgebra.CarriedPath line 12
2. theorem OAI.PolynomialVacuumAlgebra.carriedPath_of_range line 16
3. theorem OAI.PolynomialVacuumAlgebra.rightSpectators_path line 33
4. theorem OAI.PolynomialVacuumAlgebra.charge_ge_minus_one line 38
5. theorem OAI.PolynomialVacuumAlgebra.tensorExchange_carried_filtration line 40
6. theorem OAI.PolynomialVacuumAlgebra.transportCup_marked_filtration line 60