Documentation
Atlas
.
BooleanFunctions
.
code
.
Derivatives
Search
return to top
source
Imports
Init
Atlas.BooleanFunctions.code.Definitions
Mathlib.Data.Fin.Tuple.Basic
Imported by
BooleanFourier
.
discreteDerivative
source
noncomputable def
BooleanFourier
.
discreteDerivative
{
n
:
ℕ
}
(
f
:
BoolFn
(
n
+
1
)
)
(
i
:
Fin
(
n
+
1
)
)
:
BoolFn
n
Instances For