OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LitEdgesSubsetTree.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.litEdges_subset_tree line 23
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.lit_walk_active line 28
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.blockActiveSet line 40
4. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.blockActiveSet_connected line 44
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.block_gate_length line 72