OAI/Combinatorics/PolynomialVacuum/Bridge/BridgePrimitiveMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PolynomialVacuumBridge.Corridor.BridgeWord.(instance at line 8) line 8
2. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.sequences line 9
3. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.consPair_injective line 13
4. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.sequences_members line 18
5. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.sequence_height_bound line 30
6. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.sequences_mass line 43
7. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.primitive_finite_sum_le_one line 54
8. abbrev OAI.PolynomialVacuumBridge.Corridor.BridgeWord.Primitive line 91
9. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.primitive_mass_summable line 93
10. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.primitive_mass_le_one line 102