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
.