OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DataInjective.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.data_injective line 22
2. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.(instance at line 30) line 30
3. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.(instance at line 33) line 33
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listIndicator_nonneg line 37
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listIndicator_append_length line 40
6. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.witnessCount_le_joint_lists line 44