OAI/NumberTheory/Ostmann/Construction/FiniteCRTPoisson.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.cutoff_fourier_zero_outside line 10
2. theorem OAI.Ostmann.Construction.cutoff_tsum_eq_finite line 26
3. theorem OAI.Ostmann.Construction.crt_normalized_poisson_finite line 34
4. theorem OAI.Ostmann.Construction.crt_product_transform_zero line 47