Order

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

Statistics

Metric	Count
Definitions meromorphicOrderAt	1
Theorems meromorphicOrderAt_eq, meromorphicOrderAt_nonneg, of_meromorphicOrderAt_pos, analyticAt, meromorphicOrderAt_comp, analyticAt_mem_codiscreteWithin, codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, eventually_analyticAt, eventually_analyticAt_or_mem_compl, exists_meromorphicOrderAt_ne_top_iff_forall, isClopen_setOf_meromorphicOrderAt_eq_top, meromorphicOrderAt_ne_top_of_isPreconnected, eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top, meromorphicAt_of_meromorphicOrderAt_ne_zero, meromorphicOrderAt_add, meromorphicOrderAt_add_eq_left_of_lt, meromorphicOrderAt_add_eq_right_of_lt, meromorphicOrderAt_add_of_ne, meromorphicOrderAt_add_of_top_left, meromorphicOrderAt_add_of_top_right, meromorphicOrderAt_comp_of_deriv_ne_zero, meromorphicOrderAt_congr, meromorphicOrderAt_const, meromorphicOrderAt_const_intCast, meromorphicOrderAt_const_natCast, meromorphicOrderAt_const_ofNat, meromorphicOrderAt_eq_int_iff, meromorphicOrderAt_eq_top_iff, meromorphicOrderAt_id, meromorphicOrderAt_inv, meromorphicOrderAt_mul, meromorphicOrderAt_mul_of_ne_zero, meromorphicOrderAt_ne_top_iff, meromorphicOrderAt_ne_top_iff_eventually_ne_zero, meromorphicOrderAt_of_not_meromorphicAt, meromorphicOrderAt_pow, meromorphicOrderAt_smul, meromorphicOrderAt_smul_of_ne_zero, meromorphicOrderAt_zpow, tendsto_cobounded_iff_meromorphicOrderAt_neg, tendsto_cobounded_of_meromorphicOrderAt_neg, tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero, tendsto_nhds_iff_meromorphicOrderAt_nonneg, tendsto_nhds_of_meromorphicOrderAt_nonneg, tendsto_zero_iff_meromorphicOrderAt_pos, tendsto_zero_of_meromorphicOrderAt_pos	47
Total	48

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
meromorphicOrderAt_eq 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt ENat.map analyticOrderAt	—	ENat.map_top meromorphicOrderAt_eq_top_iff Filter.Eventually.filter_mono nhdsWithin_le_nhds analyticOrderAt_eq_top meromorphicOrderAt_eq_int_iff meromorphicAt zpow_natCast analyticOrderAt_eq_natCast
meromorphicOrderAt_nonneg 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing meromorphicOrderAt	—	meromorphicOrderAt_eq Int.instAddLeftMono Int.instZeroLEOneClass
of_meromorphicOrderAt_pos 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing meromorphicOrderAt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	—	MeromorphicAt.analyticAt meromorphicAt_of_meromorphicOrderAt_ne_zero LT.lt.ne' continuousAt_iff_punctured_nhds tendsto_zero_of_meromorphicOrderAt_pos

MeromorphicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt 📖	mathematical	MeromorphicAt ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedSpace	—	analyticAt_const AnalyticAt.congr ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuousAt_const PerfectSpace.not_isolated instPerfectSpace Filter.mp_mem meromorphicOrderAt_eq_top_iff Filter.univ_mem' meromorphicOrderAt_eq_int_iff tendsto_nhds_iff_meromorphicOrderAt_nonneg ContinuousWithinAt.tendsto ContinuousAt.continuousWithinAt CanLift.prf instCanLiftIntNatCastLeOfNat ContinuousAt.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousAt.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousAt_id' AnalyticAt.continuousAt zpow_natCast AnalyticAt.fun_smul IsScalarTower.left AnalyticAt.fun_pow AnalyticAt.fun_sub analyticAt_id
meromorphicOrderAt_comp 📖	mathematical	MeromorphicAt AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Filter.EventuallyConst nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	meromorphicOrderAt WithTop MulZeroClass.toMul WithTop.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing ENat.map analyticOrderAt SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	eq_or_ne WithTop.top_mul Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero AnalyticAt.analyticOrderAt_eq_zero AnalyticAt.fun_sub analyticAt_const sub_self meromorphicOrderAt_eq_top_iff Filter.eventually_map Filter.EventuallyEq.filter_mono AnalyticAt.map_nhdsNE WithTop.coe_untop₀_of_ne_top meromorphicOrderAt_ne_top_iff Filter.EventuallyEq.comp_tendsto AnalyticAt.meromorphicOrderAt_eq AnalyticAt.comp analyticOrderAt_eq_zero ENat.map_zero CharP.cast_eq_zero CharP.ofCharZero WithTop.coe_zero meromorphicOrderAt_congr meromorphicOrderAt_smul zpow fun_sub AnalyticAt.meromorphicAt const add_zero meromorphicOrderAt_zpow

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_mem_codiscreteWithin 📖	mathematical	MeromorphicOn	Set Filter Filter.instMembership Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField setOf AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedSpace	—	mem_codiscreteWithin Filter.disjoint_principal_right Filter.eventually_mem_set Filter.mp_mem eventually_analyticAt_or_mem_compl Filter.univ_mem'
codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top 📖	mathematical	MeromorphicOn	Set Set.Elem Filter Filter.instMembership Filter.codiscrete instTopologicalSpaceSubtype Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField setOf WithTop meromorphicOrderAt WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Top.top WithTop.top	—	mem_codiscrete_subtype_iff_mem_codiscreteWithin mem_codiscreteWithin Filter.disjoint_principal_right MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero Filter.mp_mem eventually_eventually_nhdsWithin Filter.univ_mem' eq_or_ne eventually_nhdsWithin_iff eventually_nhds_iff IsOpen.sdiff isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Set.mem_diff_of_mem eventually_analyticAt_or_mem_compl AnalyticAt.meromorphicOrderAt_eq AnalyticAt.analyticOrderAt_eq_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero Int.instIsOrderedAddMonoid
eventually_analyticAt 📖	mathematical	MeromorphicOn Set Set.instMembership	Filter.Eventually AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Set.instSDiff Set.instSingletonSet	—	nhdsWithin_mono MeromorphicAt.eventually_continuousAt Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' MeromorphicAt.analyticAt
eventually_analyticAt_or_mem_compl 📖	mathematical	MeromorphicOn Set Set.instMembership	Filter.Eventually AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Compl.compl Set.instCompl nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Set.instSingletonSet	—	Set.ext nhdsWithin_union Filter.mp_mem eventually_analyticAt Filter.univ_mem' self_mem_nhdsWithin
exists_meromorphicOrderAt_ne_top_iff_forall 📖	—	MeromorphicOn IsConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	—	isPreconnected_iff_preconnectedSpace IsConnected.isPreconnected isClopen_iff isClopen_setOf_meromorphicOrderAt_eq_top IsConnected.nonempty
isClopen_setOf_meromorphicOrderAt_eq_top 📖	mathematical	MeromorphicOn	IsClopen Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField setOf WithTop meromorphicOrderAt Top.top WithTop.top	—	isOpen_compl_iff isOpen_iff_forall_mem_open MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero meromorphicOrderAt_eq_top_iff eventually_nhds_iff eventually_nhdsWithin_iff Filter.not_eventually Filter.Eventually.frequently PerfectSpace.not_isolated instPerfectSpace IsOpen.sdiff isClosed_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Iff.not Set.mem_singleton_iff Subtype.coe_ne_coe isOpen_induced Set.mem_of_mem_diff Set.mem_of_mem_inter_right Set.mem_diff
meromorphicOrderAt_ne_top_of_isPreconnected 📖	—	MeromorphicOn IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set Set.instMembership	—	—	exists_meromorphicOrderAt_ne_top_iff_forall Set.nonempty_of_mem

(root)

Definitions

Name	Category	Theorems
meromorphicOrderAt 📖	CompOp	39 math math: tendsto_zero_iff_meromorphicOrderAt_pos, MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, meromorphicOrderAt_const_ofNat, tendsto_cobounded_iff_meromorphicOrderAt_neg, meromorphicOrderAt_const, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, meromorphicOrderAt_mul, meromorphicOrderAt_add_of_ne, AnalyticAt.meromorphicOrderAt_eq, meromorphicOrderAt_ne_top_iff, meromorphicOrderAt_eq_top_iff, meromorphicOrderAt_mul_of_ne_zero, meromorphicOrderAt_add, Function.FactorizedRational.meromorphicOrderAt_eq, meromorphicOrderAt_toMeromorphicNFOn, MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, meromorphicOrderAt_const_natCast, AnalyticAt.meromorphicOrderAt_nonneg, MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top, meromorphicOrderAt_id, meromorphicOrderAt_comp_of_deriv_ne_zero, tendsto_nhds_iff_meromorphicOrderAt_nonneg, meromorphicOrderAt_inv, meromorphicOrderAt_eq_int_iff, meromorphicNFAt_iff_analyticAt_or, MeromorphicOn.divisor_apply, tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero, meromorphicOrderAt_smul, PeriodPair.order_weierstrassP, meromorphicOrderAt_smul_of_ne_zero, meromorphicOrderAt_pow, eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top, meromorphicOrderAt_zpow, meromorphicOrderAt_of_not_meromorphicAt, meromorphicOrderAt_const_intCast, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, MeromorphicOn.divisor_def, meromorphicOrderAt_congr, MeromorphicAt.meromorphicOrderAt_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top 📖	mathematical	—	Filter.EventuallyConst nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet meromorphicOrderAt SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Top.top WithTop WithTop.top	—	AddTorsor.nonempty
meromorphicAt_of_meromorphicOrderAt_ne_zero 📖	mathematical	—	MeromorphicAt	—	Mathlib.Tactic.Contrapose.contrapose₂ meromorphicOrderAt_of_not_meromorphicAt
meromorphicOrderAt_add 📖	mathematical	MeromorphicAt	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder SemilatticeInf.toMin WithTop.semilatticeInf Lattice.toSemilatticeInf instLatticeInt meromorphicOrderAt Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	min_top_left meromorphicOrderAt_congr Filter.mp_mem meromorphicOrderAt_eq_top_iff Filter.univ_mem' AddRightCancelSemigroup.toIsRightCancelAdd le_refl inf_of_le_left AddLeftCancelSemigroup.toIsLeftCancelAdd CanLift.prf WithTop.canLift meromorphicOrderAt_eq_int_iff AnalyticAt.add AnalyticAt.smul NormedSpace.toIsBoundedSMul IsScalarTower.left AnalyticAt.zpow_nonneg AnalyticAt.fun_sub analyticAt_id analyticAt_const sub_nonneg covariant_swap_add_of_covariant_add Int.instAddLeftMono min_le_left min_le_right self_mem_nhdsWithin smul_add add_sub_cancel MeromorphicAt.zpow MeromorphicAt.fun_sub MeromorphicAt.id MeromorphicAt.const NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing mul_one meromorphicOrderAt_smul AnalyticAt.meromorphicAt le_add_of_nonneg_right WithTop.addLeftMono AnalyticAt.meromorphicOrderAt_nonneg
meromorphicOrderAt_add_eq_left_of_lt 📖	mathematical	MeromorphicAt WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder meromorphicOrderAt	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	meromorphicOrderAt_congr Filter.mp_mem meromorphicOrderAt_eq_top_iff Filter.univ_mem' AddLeftCancelSemigroup.toIsLeftCancelAdd CanLift.prf WithTop.canLift LT.lt.ne_top meromorphicOrderAt_eq_int_iff MeromorphicAt.add AnalyticAt.add AnalyticAt.smul NormedSpace.toIsBoundedSMul IsScalarTower.left AnalyticAt.zpow_nonneg AnalyticAt.fun_sub analyticAt_id analyticAt_const sub_nonneg covariant_swap_add_of_covariant_add Int.instAddLeftMono le_of_lt WithTop.coe_lt_coe sub_self zero_zpow sub_ne_zero LT.lt.ne' zero_smul add_zero self_mem_nhdsWithin smul_add add_sub_cancel Mathlib.Tactic.Contrapose.contrapose₄ add_sub_cancel_right MeromorphicAt.sub meromorphicOrderAt_of_not_meromorphicAt
meromorphicOrderAt_add_eq_right_of_lt 📖	mathematical	MeromorphicAt WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder meromorphicOrderAt	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add_comm meromorphicOrderAt_add_eq_left_of_lt
meromorphicOrderAt_add_of_ne 📖	mathematical	MeromorphicAt	meromorphicOrderAt Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithTop SemilatticeInf.toMin WithTop.semilatticeInf Lattice.toSemilatticeInf instLatticeInt	—	lt_or_lt_iff_ne inf_of_le_left LT.lt.le meromorphicOrderAt_add_eq_left_of_lt inf_of_le_right meromorphicOrderAt_add_eq_right_of_lt
meromorphicOrderAt_add_of_top_left 📖	mathematical	meromorphicOrderAt Top.top WithTop WithTop.top	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	meromorphicOrderAt_congr Filter.mp_mem meromorphicOrderAt_eq_top_iff Filter.univ_mem' zero_add
meromorphicOrderAt_add_of_top_right 📖	mathematical	meromorphicOrderAt Top.top WithTop WithTop.top	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add_comm meromorphicOrderAt_add_of_top_left
meromorphicOrderAt_comp_of_deriv_ne_zero 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt	—	AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero MeromorphicAt.meromorphicOrderAt_comp Nat.cast_one mul_one Int.instNontrivial meromorphicOrderAt_of_not_meromorphicAt meromorphicAt_comp_iff_of_deriv_ne_zero
meromorphicOrderAt_congr 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet	meromorphicOrderAt	—	meromorphicOrderAt_eq_top_iff Filter.EventuallyEq.rw Filter.EventuallyEq.symm meromorphicOrderAt_eq_int_iff MeromorphicAt.congr Mathlib.Tactic.Contrapose.contrapose₄ meromorphicOrderAt_of_not_meromorphicAt
meromorphicOrderAt_const 📖	mathematical	—	meromorphicOrderAt WithTop NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Top.top WithTop.top WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	meromorphicOrderAt_eq_int_iff MeromorphicAt.const analyticAt_const zpow_zero one_smul
meromorphicOrderAt_const_intCast 📖	mathematical	—	meromorphicOrderAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instIntCast AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing WithTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop.top WithTop.zero Int.instNormedCommRing	—	meromorphicOrderAt_const
meromorphicOrderAt_const_natCast 📖	mathematical	—	meromorphicOrderAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instNatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing WithTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop.top WithTop.zero Int.instNormedCommRing	—	meromorphicOrderAt_const
meromorphicOrderAt_const_ofNat 📖	mathematical	—	meromorphicOrderAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop.top WithTop.zero Int.instNormedCommRing	—	Semiring.toGrindSemiring_ofNat meromorphicOrderAt_const
meromorphicOrderAt_eq_int_iff 📖	mathematical	MeromorphicAt	meromorphicOrderAt WithTop.some AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Filter.Eventually 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 DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup nhdsWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Compl.compl Set Set.instCompl Set.instSingletonSet	—	ENat.map_top WithTop.coe_natCast WithTop.LinearOrderedAddCommGroup.top_sub eq_false_intro WithTop.top_ne_coe Filter.EventuallyEq.eq_of_nhds Filter.EventuallyEq.eq_1 AnalyticAt.frequently_eq_iff_eventually_eq analyticAt_const Filter.Eventually.frequently PerfectSpace.not_isolated instPerfectSpace eventually_nhdsWithin_iff Filter.mp_mem analyticOrderAt_eq_top Filter.univ_mem' smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass pow_ne_zero isReduced_of_noZeroDivisors sub_ne_zero zpow_ne_zero SemigroupAction.mul_smul ENat.ne_top_iff_exists ENat.map_coe WithTop.LinearOrderedAddCommGroup.coe_sub AnalyticAt.analyticOrderAt_eq_natCast zpow_add₀ add_sub_assoc add_sub_cancel_left zpow_natCast AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero
meromorphicOrderAt_eq_top_iff 📖	mathematical	—	meromorphicOrderAt Top.top WithTop WithTop.top Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet	—	Filter.mp_mem analyticOrderAt_eq_top Filter.univ_mem' smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass sub_ne_zero ENat.ne_top_iff_exists Mathlib.Tactic.Contrapose.contrapose₄ AnalyticAt.frequently_eq_iff_eventually_eq analyticAt_const Filter.Eventually.frequently PerfectSpace.not_isolated instPerfectSpace smul_zero meromorphicOrderAt_of_not_meromorphicAt MeromorphicAt.congr MeromorphicAt.const Filter.EventuallyEq.symm
meromorphicOrderAt_id 📖	mathematical	—	meromorphicOrderAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithTop WithTop.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AnalyticAt.meromorphicOrderAt_eq analyticAt_id analyticOrderAt_id Nat.cast_one
meromorphicOrderAt_inv 📖	mathematical	—	meromorphicOrderAt 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 WithTop WithTop.LinearOrderedAddCommGroup.instNeg Int.instAddCommGroup	—	Int.instIsOrderedAddMonoid LinearOrderedAddCommGroupWithTop.neg_top neg_neg meromorphicOrderAt_eq_top_iff Filter.mp_mem Filter.univ_mem' CanLift.prf WithTop.canLift meromorphicOrderAt_eq_int_iff MeromorphicAt.inv AnalyticAt.inv Iff.not inv_eq_zero eventually_nhdsWithin_iff mul_inv_rev zpow_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Contrapose.contrapose₄ inv_inv meromorphicOrderAt_of_not_meromorphicAt neg_zero
meromorphicOrderAt_mul 📖	mathematical	MeromorphicAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithTop WithTop.add	—	meromorphicOrderAt_smul
meromorphicOrderAt_mul_of_ne_zero 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	meromorphicOrderAt_smul_of_ne_zero
meromorphicOrderAt_ne_top_iff 📖	mathematical	MeromorphicAt	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Compl.compl Set Set.instCompl Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid 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 DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup WithTop.untop₀ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing meromorphicOrderAt	—	meromorphicOrderAt_eq_int_iff WithTop.coe_untop₀_of_ne_top
meromorphicOrderAt_ne_top_iff_eventually_ne_zero 📖	mathematical	MeromorphicAt	Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet	—	meromorphicOrderAt_ne_top_iff Filter.mp_mem eventually_nhdsWithin_of_eventually_nhds ContinuousAt.ne_iff_eventually_ne TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace AnalyticAt.continuousAt continuousAt_const self_mem_nhdsWithin Filter.univ_mem' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero PerfectSpace.not_isolated instPerfectSpace
meromorphicOrderAt_of_not_meromorphicAt 📖	mathematical	MeromorphicAt	meromorphicOrderAt WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	—
meromorphicOrderAt_pow 📖	mathematical	MeromorphicAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField WithTop MulZeroClass.toMul WithTop.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	pow_zero CharP.cast_eq_zero CharP.ofCharZero WithTop.charZero Int.instCharZero MulZeroClass.zero_mul WithTop.coe_zero meromorphicOrderAt_eq_int_iff MeromorphicAt.const analyticAt_const NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing zpow_zero mul_one pow_add pow_one meromorphicOrderAt_mul MeromorphicAt.pow Nat.cast_add Nat.cast_one Int.instIsOrderedAddMonoid add_top Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt
meromorphicOrderAt_smul 📖	mathematical	MeromorphicAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt 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 WithTop WithTop.add	—	Int.instIsOrderedAddMonoid top_add Filter.mp_mem Filter.univ_mem' zero_smul add_top smul_zero WithTop.coe_add meromorphicOrderAt_eq_int_iff MeromorphicAt.smul AnalyticAt.smul NormedSpace.toIsBoundedSMul IsScalarTower.left instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero self_mem_nhdsWithin SemigroupAction.mul_smul SMulCommClass.smul_comm smulCommClass_self zpow_add₀ sub_ne_zero
meromorphicOrderAt_smul_of_ne_zero 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt 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	—	meromorphicOrderAt_smul AnalyticAt.meromorphicAt AnalyticAt.meromorphicOrderAt_eq AnalyticAt.analyticOrderAt_eq_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero zero_add meromorphicOrderAt_of_not_meromorphicAt meromorphicAt_smul_iff_of_ne_zero
meromorphicOrderAt_zpow 📖	mathematical	MeromorphicAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	meromorphicOrderAt Pi.instPow DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing WithTop MulZeroClass.toMul WithTop.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing WithTop.some	—	zpow_zero MulZeroClass.zero_mul WithTop.coe_zero meromorphicOrderAt_eq_int_iff MeromorphicAt.const analyticAt_const NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing mul_one WithTop.mul_top meromorphicOrderAt_eq_top_iff Filter.mp_mem Filter.univ_mem' zero_zpow meromorphicOrderAt_ne_top_iff WithTop.coe_untop₀_of_ne_top WithTop.coe_mul MeromorphicAt.zpow AnalyticAt.zpow zpow_eq_zero_iff Pi.pow_apply smul_eq_mul mul_zpow mul_comm zpow_mul
tendsto_cobounded_iff_meromorphicOrderAt_neg 📖	mathematical	MeromorphicAt	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder meromorphicOrderAt WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	lt_or_ge tendsto_nhds_of_meromorphicOrderAt_nonneg not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.norm
tendsto_cobounded_of_meromorphicOrderAt_neg 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder meromorphicOrderAt WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	meromorphicAt_of_meromorphicOrderAt_ne_zero LT.lt.ne WithTop.ne_top_iff_exists LT.lt.ne_top meromorphicOrderAt_eq_int_iff norm_smul NormedSpace.toNormSMulClass Filter.Tendsto.atTop_mul_pos Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_nhdsWithin_iff ContinuousAt.continuousWithinAt ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousAt_id' continuousAt_const sub_self ContinuousWithinAt.tendsto Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Filter.Tendsto.comp tendsto_norm_cobounded_atTop tendsto_zpow_nhdsNE_zero_cobounded Filter.Tendsto.norm AnalyticAt.continuousAt Filter.Tendsto.congr'
tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero 📖	mathematical	MeromorphicAt	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup meromorphicOrderAt WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	eq_or_ne tendsto_ne_zero_of_meromorphicOrderAt_eq_zero Ne.lt_or_gt not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.norm tendsto_norm_atTop_iff_cobounded tendsto_cobounded_of_meromorphicOrderAt_neg tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace tendsto_zero_of_meromorphicOrderAt_pos
tendsto_ne_zero_of_meromorphicOrderAt_eq_zero 📖	mathematical	MeromorphicAt meromorphicOrderAt WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	meromorphicOrderAt_eq_int_iff Filter.Tendsto.congr' ContinuousWithinAt.tendsto ContinuousAt.continuousWithinAt AnalyticAt.continuousAt Filter.mp_mem Filter.univ_mem' zpow_zero one_smul
tendsto_nhds_iff_meromorphicOrderAt_nonneg 📖	mathematical	MeromorphicAt	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing meromorphicOrderAt	—	lt_or_ge not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.norm tendsto_norm_atTop_iff_cobounded tendsto_cobounded_of_meromorphicOrderAt_neg tendsto_nhds_of_meromorphicOrderAt_nonneg
tendsto_nhds_of_meromorphicOrderAt_nonneg 📖	mathematical	MeromorphicAt WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing meromorphicOrderAt	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	LE.le.eq_or_lt tendsto_ne_zero_of_meromorphicOrderAt_eq_zero tendsto_zero_of_meromorphicOrderAt_pos
tendsto_zero_iff_meromorphicOrderAt_pos 📖	mathematical	MeromorphicAt	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing meromorphicOrderAt	—	lt_or_ge tendsto_zero_of_meromorphicOrderAt_pos LE.le.eq_or_lt tendsto_ne_zero_of_meromorphicOrderAt_eq_zero tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PerfectSpace.not_isolated instPerfectSpace not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Tendsto.norm tendsto_norm_atTop_iff_cobounded tendsto_cobounded_of_meromorphicOrderAt_neg
tendsto_zero_of_meromorphicOrderAt_pos 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing meromorphicOrderAt	Filter.Tendsto nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	meromorphicAt_of_meromorphicOrderAt_ne_zero LT.lt.ne' Filter.Tendsto.congr' tendsto_const_nhds Filter.mp_mem meromorphicOrderAt_eq_top_iff Filter.univ_mem' meromorphicOrderAt_eq_int_iff CanLift.prf instCanLiftIntNatCastLeOfNat LT.lt.le WithTop.addLeftMono Int.instAddLeftMono WithTop.zeroLEOneClass Int.instZeroLEOneClass NeZero.charZero_one WithTop.charZero Int.instCharZero sub_self zero_pow_eq_zero IsSimpleRing.instNontrivial DivisionRing.isSimpleRing zero_smul ContinuousAt.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousAt.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousAt_id' continuousAt_const AnalyticAt.continuousAt ContinuousWithinAt.tendsto ContinuousAt.continuousWithinAt zpow_natCast

---

← Back to Index