OAI/NumberTheory/Ostmann/Construction/ZModPoisson.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Construction.finEquiv_eq_natCastline 10 - theorem
OAI.Ostmann.Construction.fourier_fin_eq_stdAddCharline 19 - theorem
OAI.Ostmann.Construction.finite_fourier_eq_dftline 29 - theorem
OAI.Ostmann.Construction.zmod_scaled_poissonline 40