Divisor

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

Statistics

Metric	Count
Definitions divisor	1
Theorems divisor_apply, 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_prod, divisor_fun_smul, divisor_fun_zpow, divisor_intCast, divisor_inv, divisor_mul, divisor_natCast, divisor_ofNat, divisor_pow, divisor_prod, 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	30
Total	31

MeromorphicOn

Definitions

Name	Category	Theorems
divisor 📖	CompOp	46 math math: ValueDistribution.logCounting_zero, Function.FactorizedRational.divisor, divisor_fun_smul, divisor_congr_codiscreteWithin_of_eqOn_compl, AnalyticOnNhd.circleAverage_log_norm, divisor_const, divisor_pow, divisor_natCast, ValueDistribution.logCounting_top, divisor_inv, divisor_fun_pow, divisor_fun_prod, divisor_sub_const_self, divisor_prod, 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, AnalyticOnNhd.sum_divisor_le, negPart_divisor_add_le_max, divisor_congr_codiscreteWithin, divisor_smul, negPart_divisor_add_le_add, AnalyticOnNhd.divisor_apply, 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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	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.instAddGroup	—	divisor_inv
divisor_fun_mul 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace 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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	divisor_smul
divisor_fun_pow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Monoid.toPow 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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	divisor_pow
divisor_fun_prod 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Finset.prod CommRing.toCommMonoid Field.toCommRing NormedField.toField Finset.sum 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.instAddCommMonoid Int.instAddCommMonoid	—	Finset.prod_apply divisor_prod
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 NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedField.toNormedSpace	—	divisor_smul
divisor_fun_zpow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace 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.instAddGroup	—	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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	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.instAddGroup	—	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 NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace 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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	Semiring.toGrindSemiring_ofNat divisor_const
divisor_pow 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instPow Monoid.toPow 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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	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_prod 📖	mathematical	MeromorphicOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	divisor NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Finset.prod Pi.commMonoid CommRing.toCommMonoid Field.toCommRing NormedField.toField Finset.sum 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.instAddCommMonoid Int.instAddCommMonoid	—	Finset.induction Finset.prod_empty Finset.sum_empty divisor_ofNat meromorphicOrderAt_prod Finset.mem_insert_of_mem Finset.prod_insert Finset.sum_insert divisor_mul prod Finset.mem_insert_self
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 NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedField.toNormedSpace	—	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 NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace 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.instAddGroup	—	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 Function.locallyFinsuppWithin.instAddGroup Int.instAddGroup divisor Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Function.locallyFinsuppWithin.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT
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 Function.locallyFinsuppWithin.instAddGroup Int.instAddGroup 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 instReflLe 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 NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt Function.locallyFinsuppWithin.instAddGroup Int.instAddGroup 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 NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt Function.locallyFinsuppWithin.instAddGroup Int.instAddGroup 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_apply 📖	mathematical	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace 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 MeromorphicOn.divisor WithTop.untop₀ ENat.map analyticOrderAt	—	MeromorphicOn.divisor_apply AnalyticOnNhd.meromorphicOn AnalyticAt.meromorphicOrderAt_eq
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 NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin.instLE Function.locallyFinsuppWithin.instZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid MeromorphicOn.divisor	—	MeromorphicOn.divisor_apply AnalyticOnNhd.meromorphicOn AnalyticAt.meromorphicOrderAt_nonneg Function.locallyFinsuppWithin.apply_eq_zero_of_notMem instReflLe

---

← Back to Index