Manifold

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

Statistics

Metric	Count
Definitions instChartedSpaceComplex, smulFDeriv	2
Theorems analyticAt_smul, contMDiffAt_iff, contMDiffAt_ofComplex, contMDiff_coe, contMDiff_denom, contMDiff_denom_zpow, contMDiff_inv_denom, contMDiff_num, contMDiff_smul, deriv_smul, deriv_smul_ne_zero, det_smulFDeriv, eq_zero_of_frequently, hasStrictDerivAt_smul, hasStrictFDerivAt_smul, instIsManifoldComplexModelWithCornersSelfTopWithTopENat, mdifferentiableAt_iff, mdifferentiableAt_ofComplex, mdifferentiable_coe, mdifferentiable_denom, mdifferentiable_denom_zpow, mdifferentiable_iff, mdifferentiable_inv_denom, mdifferentiable_num, mdifferentiable_smul, meromorphicOrderAt_comp_smul, mul_eq_zero_iff, prod_eq_zero_iff, smulFDeriv_J_mul	29
Total	31

UpperHalfPlane

Definitions

Name	Category	Theorems
instChartedSpaceComplex 📖	CompOp	29 math math: mdifferentiable_num, CuspFormClass.holo, mdifferentiable_inv_denom, contMDiff_coe, CuspForm.holo', contMDiff_inv_denom, contMDiff_num, mdifferentiable_denom, MDifferentiable.slash, contMDiff_denom_zpow, Derivative.normalizedDerivOfComplex_mdifferentiable, mdifferentiable_jacobiTheta, contMDiffAt_ofComplex, ModularForm.holo', contMDiffAt_iff, instIsManifoldComplexModelWithCornersSelfTopWithTopENat, mdifferentiable_coe, ModularFormClass.holo, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, mdifferentiableAt_iff, contMDiff_smul, contMDiff_denom, E2_mdifferentiable, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, mdifferentiable_denom_zpow, Derivative.serreDerivative_mdifferentiable, mdifferentiable_iff, mdifferentiableAt_ofComplex, mdifferentiable_smul
smulFDeriv 📖	CompOp	3 math math: smulFDeriv_J_mul, hasStrictFDerivAt_smul, det_smulFDeriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_smul 📖	mathematical	Real Real.instLT Real.instZero Matrix.det Fin.fintype Real.commRing Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex	—	DifferentiableOn.analyticAt Complex.instCompleteSpace DifferentiableAt.differentiableWithinAt MDifferentiable.mdifferentiableAt MDifferentiable.comp mdifferentiable_coe mdifferentiable_smul IsOpen.mem_nhds isOpen_upperHalfPlaneSet im_pos
contMDiffAt_iff 📖	mathematical	—	ContMDiffAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf ContDiffAt OpenPartialHomeomorph.toFun' ofComplex coe	—	contMDiffAt_iff_contDiffAt ContMDiffAt.comp ofComplex_apply contMDiffAt_ofComplex im_pos contMDiff_coe
contMDiffAt_ofComplex 📖	mathematical	Real Real.instLT Real.instZero Complex.im	ContMDiffAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf chartedSpaceSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex OpenPartialHomeomorph.toFun' ofComplex	—	contMDiffAt_iff ContinuousAt.eq_1 nhds_induced Filter.tendsto_comap_iff Filter.Tendsto.congr' Filter.EventuallyEq.symm eventuallyEq_coe_comp_ofComplex ofComplex_apply_of_im_pos Filter.tendsto_id isOpenEmbedding_coe PartialEquiv.trans_refl CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Set.range_id ContDiffAt.congr_of_eventuallyEq contDiffAt_id
contMDiff_coe 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf coe	—	contMDiffAt_extChartAt
contMDiff_denom 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf denom coe	—	ContMDiff.add instContMDiffAddSelf ContMDiff.smul contMDiff_const contMDiff_coe
contMDiff_denom_zpow 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf DivInvMonoid.toZPow Complex.instDivInvMonoid denom coe	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_zpow isOpen_compl_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace denom_ne_zero ContMDiffAt.comp ContDiffAt.contMDiffAt AnalyticAt.contDiffAt contMDiff_denom
contMDiff_inv_denom 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf Complex.instInv denom coe	—	zpow_neg zpow_one contMDiff_denom_zpow
contMDiff_num 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf num coe	—	ContMDiff.add instContMDiffAddSelf ContMDiff.smul contMDiff_const contMDiff_coe
contMDiff_smul 📖	mathematical	Real Real.instLT Real.instZero Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction	—	contMDiffAt_iff_target Continuous.continuousAt ContinuousConstSMul.continuous_const_smul instContinuousGLSMul im_pos coe_smul_of_det_pos isOpenEmbedding_coe glPos_smul_def PartialEquiv.trans_refl ContMDiffAt.mul instContMDiffMulOfTopWithTopENat ContMDiffRing.toContMDiffMul instFieldContMDiffRing contMDiff_num contMDiff_inv_denom
deriv_smul 📖	mathematical	Real Real.instLT Real.instZero Matrix.det Fin.fintype Real.commRing Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring	deriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction OpenPartialHomeomorph.toFun' instTopologicalSpace ofComplex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.ofReal Matrix.det Real.commRing Units.val Monoid.toPow Complex.instSemiring denom	—	HasDerivAt.deriv HasStrictDerivAt.hasDerivAt hasStrictDerivAt_smul
deriv_smul_ne_zero 📖	—	Real Real.instLT Real.instZero Matrix.det Fin.fintype Real.commRing Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring	—	—	deriv_smul div_ne_zero Nat.cast_zero LT.lt.ne' pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass denom_ne_zero
det_smulFDeriv 📖	mathematical	—	ContinuousLinearMap.det Real Real.commRing Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex smulFDeriv DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul SignType.cast Real.instZero Real.instOne Real.instNeg DFunLike.coe OrderHom SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Monoid.toPow Real.instMonoid Norm.norm Complex.instNorm denom	—	RingHomInvPair.ids Ne.lt_or_gt Matrix.GeneralLinearGroup.det_ne_zero Real.instNontrivial ContinuousLinearMap.comp.congr_simp LT.lt.not_gt LinearMap.det_comp Complex.det_conjAe LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right LinearMap.det_restrictScalars Module.Free.of_divisionRing Module.Free.self Algebra.norm_complex_eq LinearMap.det_ring one_mul map_div₀ MonoidWithZeroHom.monoidWithZeroHomClass Complex.normSq_eq_norm_sq Complex.norm_real sq_abs norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass neg_mul sign_neg SignType.coe_neg neg_div ContinuousLinearMap.id_comp sign_pos
eq_zero_of_frequently 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf Filter.Frequently Complex.instZero nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	Pi.instZero UpperHalfPlane Complex Complex.instZero	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace mdifferentiable_iff isOpen_upperHalfPlaneSet ofComplex_apply AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero IsConnected.isPreconnected Complex.isConnected_of_upperHalfPlane subset_rfl Set.instReflSubset coe_im_pos Mathlib.Tactic.Contrapose.contrapose₁ eventually_nhdsWithin_iff Filter.mp_mem Filter.eventually_map Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_coe Filter.univ_mem' im_pos
hasStrictDerivAt_smul 📖	mathematical	Real Real.instLT Real.instZero Matrix.det Fin.fintype Real.commRing Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring	HasStrictDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField Complex.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix Matrix.semiring MulAction.toSemigroupAction glAction OpenPartialHomeomorph.toFun' instTopologicalSpace ofComplex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.ofReal Matrix.det Real.commRing Units.val Monoid.toPow denom	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Matrix.det_fin_two Complex.ofReal_sub Complex.ofReal_mul mul_one Mathlib.Tactic.Ring.of_eq 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.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.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add HasStrictDerivAt.div HasStrictDerivAt.add_const HasStrictDerivAt.const_mul hasStrictDerivAt_id denom_ne_zero HasStrictDerivAt.congr_of_eventuallyEq Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_coe Filter.eventuallyEq_map coe_smul_of_det_pos ofComplex_apply
hasStrictFDerivAt_smul 📖	mathematical	—	HasStrictFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Complex Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing coe Matrix.GeneralLinearGroup Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction OpenPartialHomeomorph.toFun' instTopologicalSpace ofComplex smulFDeriv	—	LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasStrictFDerivAt.restrictScalars HasStrictDerivAt.hasStrictFDerivAt hasStrictDerivAt_smul RingHomInvPair.ids ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.id_comp Ne.lt_or_gt Units.ne_zero Real.instNontrivial RingHomCompTriple.ids SeminormedAddCommGroup.toIsTopologicalAddGroup SemigroupAction.mul_smul coe_J_smul map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd neg_neg ContinuousLinearMap.ext smulFDeriv_J_mul ContinuousLinearMap.comp_neg ContinuousLinearMap.neg_comp HasStrictFDerivAt.comp HasStrictFDerivAt.neg ContinuousLinearEquiv.hasStrictFDerivAt map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass det_J neg_mul one_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
instIsManifoldComplexModelWithCornersSelfTopWithTopENat 📖	mathematical	—	IsManifold Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Top.top WithTop ENat WithTop.top UpperHalfPlane instTopologicalSpace instChartedSpaceComplex	—	Topology.IsOpenEmbedding.isManifold_singleton isOpenEmbedding_coe
mdifferentiableAt_iff 📖	mathematical	—	MDifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf DifferentiableAt Complex.addCommGroup Complex.instModuleSelf OpenPartialHomeomorph.toFun' ofComplex coe	—	mdifferentiableAt_iff_differentiableAt MDifferentiableAt.comp ofComplex_apply mdifferentiableAt_ofComplex im_pos mdifferentiable_coe
mdifferentiableAt_ofComplex 📖	mathematical	Real Real.instLT Real.instZero Complex.im	MDifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf chartedSpaceSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex OpenPartialHomeomorph.toFun' ofComplex	—	ContMDiffAt.mdifferentiableAt contMDiffAt_ofComplex one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_coe 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf coe	—	ContMDiff.mdifferentiable contMDiff_coe one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_denom 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf denom coe	—	ContMDiff.mdifferentiable contMDiff_denom one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_denom_zpow 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf DivInvMonoid.toZPow Complex.instDivInvMonoid denom coe	—	ContMDiff.mdifferentiable contMDiff_denom_zpow one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_iff 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf DifferentiableOn Complex.addCommGroup Complex.instModuleSelf OpenPartialHomeomorph.toFun' ofComplex setOf Real Real.instLT Real.instZero Complex.im	—	DifferentiableAt.differentiableWithinAt mdifferentiableAt_iff DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds isOpen_upperHalfPlaneSet
mdifferentiable_inv_denom 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf Complex.instInv denom coe	—	ContMDiff.mdifferentiable contMDiff_inv_denom one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_num 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf num coe	—	ContMDiff.mdifferentiable contMDiff_num one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_smul 📖	mathematical	Real Real.instLT Real.instZero Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction	—	ContMDiff.mdifferentiable contMDiff_smul one_ne_zero NeZero.charZero_one WithTop.charZero
meromorphicOrderAt_comp_smul 📖	mathematical	Real Real.instLT Real.instZero Matrix.det Fin.fintype Real.commRing Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring	meromorphicOrderAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex coe	—	ofComplex_apply meromorphicOrderAt_comp_of_deriv_ne_zero analyticAt_smul deriv_smul_ne_zero Complex.instCompleteSpace Complex.instCharZero
mul_eq_zero_iff 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf	Pi.instMul UpperHalfPlane Complex Complex.instMul Pi.instZero Complex.instZero	—	eq_zero_of_frequently Filter.frequently_or_distrib Filter.Frequently.of_forall PerfectSpace.not_isolated instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial T4Space.toT1Space instT4Space PathConnectedSpace.connectedSpace ContractibleSpace.instPathConnectedSpace instContractibleSpace instNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
prod_eq_zero_iff 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex chartedSpaceSelf	Finset.prod Pi.commMonoid UpperHalfPlane Complex CommRing.toCommMonoid Complex.commRing Pi.instZero Complex.instZero Finset SetLike.instMembership Finset.instSetLike	—	Filter.Frequently.of_forall PerfectSpace.not_isolated instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial T4Space.toT1Space instT4Space PathConnectedSpace.connectedSpace ContractibleSpace.instPathConnectedSpace instContractibleSpace instNontrivial Finset.prod_apply eq_zero_of_frequently Complex.instNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Finset.prod_eq_zero
smulFDeriv_J_mul 📖	mathematical	—	smulFDeriv Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring J ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex ContinuousLinearMap.neg Real.instRing Complex.addCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.comp RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids NormedSpace.complexToReal NormedField.toNormedSpace Complex.conjCLE	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomCompTriple.ids RingHomInvPair.ids ContinuousLinearMap.comp.congr_simp map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass det_J neg_mul one_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.not_gt ContinuousLinearMap.restrictScalars.congr_simp ContinuousLinearMap.toSpanSingleton.congr_simp Complex.ofReal_neg denom_J_mul neg_div mul_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_div₀ RingHomClass.toMonoidWithZeroHomClass Complex.conj_ofReal map_pow MonoidWithZeroHomClass.toMonoidHomClass ContinuousLinearMap.id_comp Ne.lt_or_gt Matrix.GeneralLinearGroup.det_ne_zero Real.instNontrivial RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd

---

← Back to Index