OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ActiveComponents.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.activeComponents line 17
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.lit_components_subset_active line 22
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.activeConnected_iff_card line 30
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.lit_components_le_one line 45
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.unlitOccurrences line 51
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ghosts_le_unlit line 54
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedPieces_card_le line 64
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tagged_fixed_card line 68
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.free_tree_card_le_one line 104
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeCorrupted line 110
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tagged_free_card line 113