OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/NatKernelSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySparseRows.nat_kernel_sum line 14
2. lemma OAI.OrdinarySparseRows.floor_inj_of_separated line 49
3. lemma OAI.OrdinarySparseRows.nonneg_side_row line 67
4. lemma OAI.OrdinarySparseRows.separated_row line 84