OAI/Combinatorics/HoneycombCorridor/CollisionGrouping.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialVacuumBridge.Corridor.sum_record_three line 10
2. theorem OAI.PolynomialVacuumBridge.Corridor.collision_splice_surjective line 24
3. theorem OAI.PolynomialVacuumBridge.Corridor.spliceRecord_terminal line 102
4. theorem OAI.PolynomialVacuumBridge.Corridor.collision_splice_injective line 109
5. def OAI.PolynomialVacuumBridge.Corridor.collisionData line 137
6. theorem OAI.PolynomialVacuumBridge.Corridor.mem_collisionData line 143
7. theorem OAI.PolynomialVacuumBridge.Corridor.collisionData_sum line 161
8. theorem OAI.PolynomialVacuumBridge.Corridor.collision_sum_grouped line 174