Library Coq.fourier.Fourier




Require Export LegacyRing.
Require Export LegacyField.
Require Export DiscrR.
Require Export Fourier_util.

Ltac fourier := abstract (fourierz; field; discrR).

Ltac fourier_eq := apply Rge_antisym; fourier.