Documentation
LeanPool
.
LeanModularForms
.
Modularforms
.
MDifferentiableFunProp
Search
return to top
source
Imports
Init
Mathlib.Tactic.FunProp
LeanPool.LeanModularForms.Modularforms.Eisenstein
Mathlib.Geometry.Manifold.Notation
Mathlib.Geometry.Manifold.MFDeriv.Defs
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Imported by
E₄_MDifferentiable
E₆_MDifferentiable
MDifferentiableFunProp
#
source
theorem
E₄_MDifferentiable
:
MDiff
E₄
.
toFun
source
theorem
E₆_MDifferentiable
:
MDiff
E₆
.
toFun