MDifferentiable

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/MDifferentiable.lean

Statistics

Metric	Count
Definitions	0
Theorems E2_mdifferentiable	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
E2_mdifferentiable 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex chartedSpaceSelf EisensteinSeries.E2	—	UpperHalfPlane.mdifferentiable_iff DifferentiableAt.differentiableWithinAt ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet DifferentiableOn.div DifferentiableOn.deriv Complex.instCompleteSpace UpperHalfPlane.isOpen_upperHalfPlaneSet ModularForm.eta_ne_zero DifferentiableOn.congr Nat.instAtLeastTwoHAddOfNat DifferentiableOn.const_mul UpperHalfPlane.ofComplex_apply_of_im_pos inv_div ModularForm.logDeriv_eta_eq_E2 Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial

---

← Back to Index