Divisor

📁 Source: Mathlib/Analysis/Meromorphic/Divisor.lean

Statistics

Metric	Count
Definitions divisor	1
Theorems divisor_nonneg, divisor_apply, divisor_congr_codiscreteWithin, divisor_congr_codiscreteWithin_of_eqOn_compl, divisor_const, divisor_def, divisor_fun_inv, divisor_fun_mul, divisor_fun_pow, divisor_fun_smul, divisor_fun_zpow, divisor_intCast, divisor_inv, divisor_mul, divisor_natCast, divisor_ofNat, divisor_pow, divisor_restrict, divisor_smul, divisor_sub_const_of_ne, divisor_sub_const_self, divisor_zpow, min_divisor_le_divisor_add, negPart_divisor_add_le_add, negPart_divisor_add_le_max, negPart_divisor_add_of_analyticNhdOn_left, negPart_divisor_add_of_analyticNhdOn_right	27
Total	28

MeromorphicOn

Definitions

Name	Category	Theorems
divisor 📖	CompOp	41 math math: ValueDistribution.logCounting_zero, Function.FactorizedRational.divisor, divisor_fun_smul, divisor_congr_codiscreteWithin_of_eqOn_compl, divisor_const, divisor_pow, divisor_natCast, ValueDistribution.logCounting_top, divisor_inv, divisor_fun_pow, divisor_sub_const_self, divisor_intCast, divisor_sub_const_of_ne, negPart_divisor_add_of_analyticNhdOn_right, Function.locallyFinsuppWithin.toClosedBall_divisor, negPart_divisor_add_of_analyticNhdOn_left, divisor_ofNat, divisor_fun_zpow, divisor_apply, divisor_fun_mul, divisor_zpow, ValueDistribution.characteristic_sub_characteristic_inv, divisor_restrict, divisor_of_toMeromorphicNFOn, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, locallyFinsuppWithin.logCounting_divisor, divisor_fun_inv, MeromorphicNFOn.zero_set_eq_divisor_support, circleAverage_log_norm, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, AnalyticOnNhd.divisor_nonneg, min_divisor_le_divisor_add, extract_zeros_poles, negPart_divisor_add_le_max, divisor_congr_codiscreteWithin, divisor_smul, negPart_divisor_add_le_add, divisor_def, ValueDistribution.logCounting_coe, ValueDistribution.log_counting_zero_sub_logCounting_top, divisor_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisor_apply 📖	mathematical	MeromorphicOn Set Set.instMembership	DFunLike.coe Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instFunLike divisor WithTop.untop₀ meromorphicOrderAt	—	—
divisor_congr_codiscreteWithin 📖	mathematical	Filter.EventuallyEq Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField IsOpen	divisor	—	Function.locallyFinsuppWithin.ext divisor_apply congr_codiscreteWithin meromorphicOrderAt_congr mem_nhdsWithin Set.inter_subset_left Filter.mp_mem Filter.univ_mem' Function.locallyFinsuppWithin.apply_eq_zero_of_notMem Iff.not meromorphicOn_congr_codiscreteWithin
divisor_congr_codiscreteWithin_of_eqOn_compl 📖	mathematical	MeromorphicOn Filter.EventuallyEq Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set.EqOn Compl.compl Set Set.instCompl	divisor	—	Function.locallyFinsuppWithin.ext divisor_apply congr_codiscreteWithin_of_eqOn_compl meromorphicOrderAt_congr Filter.mp_mem Filter.univ_mem' Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
divisor_const 📖	mathematical	—	divisor Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instZero Int.instAddCommGroup	—	Function.locallyFinsuppWithin.ext meromorphicOrderAt_const Int.instIsOrderedAddMonoid
divisor_def 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instFunLike divisor MeromorphicOn Set Set.instMembership WithTop.untop₀ meromorphicOrderAt	—	—
divisor_fun_inv 📖	mathematical	—	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield NormedField.toField Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instNeg Int.instAddCommGroup	—	divisor_inv
divisor_fun_mul 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Int.instNormedCommRing Function.locallyFinsuppWithin.instAdd Int.instAddCommGroup	—	divisor_smul
divisor_fun_pow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instSMulNat Int.instAddCommGroup	—	divisor_pow
divisor_fun_smul 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instAdd Int.instAddCommGroup	—	divisor_smul
divisor_fun_zpow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instSMulInt Int.instAddCommGroup	—	divisor_zpow
divisor_intCast 📖	mathematical	—	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instIntCast AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instZero Int.instAddCommGroup	—	divisor_const
divisor_inv 📖	mathematical	—	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield NormedField.toField Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instNeg Int.instAddCommGroup	—	Function.locallyFinsuppWithin.ext divisor_apply meromorphicOrderAt_inv WithTop.untop₀_neg neg_zero
divisor_mul 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Int.instNormedCommRing Function.locallyFinsuppWithin.instAdd Int.instAddCommGroup	—	divisor_smul
divisor_natCast 📖	mathematical	—	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instNatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instZero Int.instAddCommGroup	—	divisor_const
divisor_ofNat 📖	mathematical	—	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instZero Int.instAddCommGroup	—	Semiring.toGrindSemiring_ofNat divisor_const
divisor_pow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instSMulNat Int.instAddCommGroup	—	Function.locallyFinsuppWithin.ext pow_zero divisor_ofNat zero_nsmul divisor_apply pow meromorphicOrderAt_pow WithTop.untop₀_mul Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
divisor_restrict 📖	mathematical	MeromorphicOn Set Set.instHasSubset	Function.locallyFinsuppWithin.restrict UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing divisor	—	Function.locallyFinsuppWithin.ext Function.locallyFinsuppWithin.restrict_apply divisor_apply mono_set Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
divisor_smul 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor Pi.smul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instAdd Int.instAddCommGroup	—	Function.locallyFinsuppWithin.ext CanLift.prf WithTop.canLift divisor_apply smul meromorphicOrderAt_smul Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
divisor_sub_const_of_ne 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instFunLike divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedField.toNormedSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	divisor_apply fun_sub id const WithTop.untop₀_coe meromorphicOrderAt_eq_int_iff MeromorphicAt.fun_sub MeromorphicAt.id MeromorphicAt.const AnalyticAt.fun_sub analyticAt_id analyticAt_const sub_ne_zero_of_ne zpow_zero one_mul Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
divisor_sub_const_self 📖	mathematical	Set Set.instMembership	DFunLike.coe Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instFunLike divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedField.toNormedSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	divisor_apply fun_sub id const WithTop.untop₀_coe meromorphicOrderAt_eq_int_iff MeromorphicAt.fun_sub MeromorphicAt.id MeromorphicAt.const analyticAt_const NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing zpow_one mul_one
divisor_zpow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor Pi.instPow DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instSMulInt Int.instAddCommGroup	—	Function.locallyFinsuppWithin.ext zpow_zero divisor_ofNat zero_smul divisor_apply zpow meromorphicOrderAt_zpow WithTop.untop₀_mul Function.locallyFinsuppWithin.apply_eq_zero_of_notMem
min_divisor_le_divisor_add 📖	mathematical	MeromorphicOn Set Set.instMembership	DFunLike.coe Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instFunLike divisor Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	divisor_apply add WithTop.untop₀_top meromorphicOrderAt_add_of_top_left meromorphicOrderAt_add_of_top_right WithTop.untop₀_min WithTop.untop₀_le_untop₀ meromorphicOrderAt_add
negPart_divisor_add_le_add 📖	mathematical	MeromorphicOn	Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instLE NegPart.negPart instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Int.instAddCommGroup divisor Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Function.locallyFinsuppWithin.instAdd	—	negPart_divisor_add_le_max sup_of_le_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Function.locallyFinsuppWithin.instIsOrderedAddMonoid Int.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd
negPart_divisor_add_le_max 📖	mathematical	MeromorphicOn	Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instLE NegPart.negPart instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Int.instAddCommGroup divisor Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Function.locallyFinsuppWithin.instMaxOfSemilatticeSup Lattice.toSemilatticeSup	—	Function.locallyFinsuppWithin.apply_eq_zero_of_notMem divisor_apply add WithTop.untop₀_top negPart_of_nonpos Int.instAddLeftMono neg_zero negPart_min covariant_swap_add_of_covariant_add le_iff_posPart_negPart min_divisor_le_divisor_add
negPart_divisor_add_of_analyticNhdOn_left 📖	mathematical	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace MeromorphicOn	NegPart.negPart Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Int.instAddCommGroup divisor Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add_comm negPart_divisor_add_of_analyticNhdOn_right
negPart_divisor_add_of_analyticNhdOn_right 📖	mathematical	MeromorphicOn AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	NegPart.negPart Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Int.instAddCommGroup divisor Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Function.locallyFinsuppWithin.ext le_inf AnalyticAt.meromorphicOrderAt_nonneg meromorphicOrderAt_add AnalyticAt.meromorphicAt sup_of_le_right Int.instAddLeftMono meromorphicOrderAt_add_eq_left_of_lt AnalyticOnNhd.meromorphicOn divisor_apply add Function.locallyFinsuppWithin.apply_eq_zero_of_notMem

MeromorphicOn.AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisor_nonneg 📖	mathematical	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instLE Function.locallyFinsuppWithin.instZero Int.instAddCommGroup MeromorphicOn.divisor	—	MeromorphicOn.divisor_apply AnalyticOnNhd.meromorphicOn AnalyticAt.meromorphicOrderAt_nonneg Function.locallyFinsuppWithin.apply_eq_zero_of_notMem

---

← Back to Index