Documentation
LeanPool
.
LeanModularForms
.
Modularforms
.
MDifferentiableFunProp
Search
return to top
source
Imports
Init
LeanPool.LeanModularForms.Modularforms.Eisenstein
Imported by
E₄_MDifferentiable
E₆_MDifferentiable
MDifferentiableFunProp
#
source
theorem
E₄_MDifferentiable
:
MDiff
E₄
.
toFun
source
theorem
E₆_MDifferentiable
:
MDiff
E₆
.
toFun