Documentation
SpherePacking
.
ForMathlib
.
MDifferentiableFunProp
Search
return to top
source
Imports
Init
Mathlib.Tactic.FunProp
SpherePacking.ModularForms.Eisenstein
Mathlib.Geometry.Manifold.MFDeriv.Defs
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Imported by
E₄_MDifferentiable
E₆_MDifferentiable
source
theorem
E₄_MDifferentiable
:
MDifferentiable
(
modelWithCornersSelf
ℂ
ℂ
)
(
modelWithCornersSelf
ℂ
ℂ
)
E₄
.
toFun
source
theorem
E₆_MDifferentiable
:
MDifferentiable
(
modelWithCornersSelf
ℂ
ℂ
)
(
modelWithCornersSelf
ℂ
ℂ
)
E₆
.
toFun