Derivative

📁 Source: Mathlib/NumberTheory/ModularForms/Derivative.lean

Statistics

Metric	Count
Definitions normalizedDerivOfComplex, serreDerivative, termD	3
Theorems normalizedDerivOfComplex_add, normalizedDerivOfComplex_const, normalizedDerivOfComplex_mdifferentiable, normalizedDerivOfComplex_mul, normalizedDerivOfComplex_neg, normalizedDerivOfComplex_pow, normalizedDerivOfComplex_smul, normalizedDerivOfComplex_sub, serreDerivative_add, serreDerivative_apply, serreDerivative_eq, serreDerivative_mdifferentiable, serreDerivative_mul, serreDerivative_smul, serreDerivative_sub	15
Total	18

Derivative

Definitions

Name	Category	Theorems
normalizedDerivOfComplex 📖	CompOp	10 math math: serreDerivative_apply, normalizedDerivOfComplex_smul, normalizedDerivOfComplex_sub, normalizedDerivOfComplex_const, normalizedDerivOfComplex_mul, normalizedDerivOfComplex_mdifferentiable, normalizedDerivOfComplex_neg, normalizedDerivOfComplex_add, normalizedDerivOfComplex_pow, serreDerivative_eq
serreDerivative 📖	CompOp	7 math math: serreDerivative_smul, serreDerivative_apply, serreDerivative_add, serreDerivative_sub, serreDerivative_mul, serreDerivative_mdifferentiable, serreDerivative_eq
termD 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalizedDerivOfComplex_add 📖	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	normalizedDerivOfComplex Pi.instAdd UpperHalfPlane Complex Complex.instAdd	—	UpperHalfPlane.mdifferentiableAt_iff deriv_add mul_add Distrib.leftDistribClass
normalizedDerivOfComplex_const 📖	mathematical	—	normalizedDerivOfComplex Pi.instZero UpperHalfPlane Complex Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat mul_inv_rev Complex.inv_I neg_mul deriv_const MulZeroClass.mul_zero
normalizedDerivOfComplex_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	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 normalizedDerivOfComplex	—	UpperHalfPlane.mdifferentiable_iff Nat.instAtLeastTwoHAddOfNat mul_inv_rev Complex.inv_I neg_mul DifferentiableOn.const_mul DifferentiableOn.deriv Complex.instCompleteSpace UpperHalfPlane.isOpen_upperHalfPlaneSet DifferentiableOn.congr UpperHalfPlane.ofComplex_apply_of_im_pos
normalizedDerivOfComplex_mul 📖	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	normalizedDerivOfComplex Pi.instMul UpperHalfPlane Complex Complex.instMul Pi.instAdd Complex.instAdd	—	UpperHalfPlane.mdifferentiableAt_iff deriv_mul mul_inv_rev Complex.inv_I neg_mul UpperHalfPlane.ofComplex_apply mul_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero
normalizedDerivOfComplex_neg 📖	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	normalizedDerivOfComplex Pi.instNeg UpperHalfPlane Complex Complex.instNeg	—	neg_mul one_mul normalizedDerivOfComplex_smul
normalizedDerivOfComplex_pow 📖	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	normalizedDerivOfComplex Pi.instPow UpperHalfPlane Complex Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Pi.instMul Complex.instMul Pi.instNatCast Complex.instNatCast	—	UpperHalfPlane.mdifferentiableAt_iff deriv_pow mul_inv_rev Complex.inv_I neg_mul UpperHalfPlane.ofComplex_apply mul_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one
normalizedDerivOfComplex_smul 📖	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	normalizedDerivOfComplex Complex Function.hasSMul UpperHalfPlane Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	UpperHalfPlane.mdifferentiableAt_iff deriv_const_smul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing smul_eq_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul
normalizedDerivOfComplex_sub 📖	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	normalizedDerivOfComplex Pi.instSub UpperHalfPlane Complex Complex.instSub	—	UpperHalfPlane.mdifferentiableAt_iff deriv_sub mul_sub
serreDerivative_add 📖	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	serreDerivative Pi.instAdd UpperHalfPlane Complex Complex.instAdd	—	Nat.instAtLeastTwoHAddOfNat normalizedDerivOfComplex_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero Mathlib.Tactic.Ring.add_pf_add_gt
serreDerivative_apply 📖	mathematical	—	serreDerivative Complex Complex.instSub normalizedDerivOfComplex Complex.instMul Complex.instInv instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat EisensteinSeries.E2	—	—
serreDerivative_eq 📖	mathematical	—	serreDerivative Complex Complex.instSub normalizedDerivOfComplex Complex.instMul Complex.instInv instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat EisensteinSeries.E2	—	—
serreDerivative_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	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 serreDerivative	—	MDifferentiable.sub normalizedDerivOfComplex_mdifferentiable Nat.instAtLeastTwoHAddOfNat mul_comm mul_left_comm mul_assoc MDifferentiable.mul mdifferentiable_const E2_mdifferentiable
serreDerivative_mul 📖	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	serreDerivative Complex Complex.instAdd Pi.instMul UpperHalfPlane Complex.instMul Pi.instAdd	—	Nat.instAtLeastTwoHAddOfNat normalizedDerivOfComplex_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero
serreDerivative_smul 📖	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	serreDerivative Complex Function.hasSMul UpperHalfPlane Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	Nat.instAtLeastTwoHAddOfNat normalizedDerivOfComplex_smul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero
serreDerivative_sub 📖	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	serreDerivative Pi.instSub UpperHalfPlane Complex Complex.instSub	—	Nat.instAtLeastTwoHAddOfNat normalizedDerivOfComplex_sub Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.nnrat_rawCast add_zero Mathlib.Tactic.Ring.add_pf_add_gt

---

← Back to Index