Basic

📁 Source: Mathlib/Analysis/Polynomial/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_div_tendsto_atBot_atTop_of_degree_gt, abs_div_tendsto_atTop_atTop_of_degree_gt, abs_div_tendsto_atTop_of_degree_gt, abs_isBoundedUnder_iff, abs_tendsto_atBot, abs_tendsto_atBot_iff, abs_tendsto_atTop, abs_tendsto_atTop_iff, div_tendsto_atBot_leadingCoeff_div_of_degree_eq, div_tendsto_atBot_of_degree_gt, div_tendsto_atBot_of_degree_gt', div_tendsto_atBot_zero_iff_degree_lt, div_tendsto_atBot_zero_of_degree_lt, div_tendsto_atTop_leadingCoeff_div_of_degree_eq, div_tendsto_atTop_of_degree_gt, div_tendsto_atTop_of_degree_gt', div_tendsto_atTop_zero_iff_degree_lt, div_tendsto_atTop_zero_of_degree_lt, div_tendsto_leadingCoeff_div_of_degree_eq, div_tendsto_zero_iff_degree_lt, div_tendsto_zero_of_degree_lt, eventually_atBot_not_isRoot, eventually_atTop_not_isRoot, eventually_no_roots, isBigO_atBot_of_degree_le, isBigO_atTop_of_degree_le, isBigO_of_degree_le, isBoundedUnder_abs_atBot_iff, isBoundedUnder_abs_atTop_iff, isEquivalent_atBot_div, isEquivalent_atBot_lead, isEquivalent_atTop_div, isEquivalent_atTop_lead, isLittleO_atBot_of_degree_lt, isLittleO_atTop_of_degree_lt, tendsto_atBot_iff_leadingCoeff_nonpos, tendsto_atBot_of_leadingCoeff_nonpos, tendsto_atTop_iff_leadingCoeff_nonneg, tendsto_atTop_of_leadingCoeff_nonneg, tendsto_nhds_iff	40
Total	40

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_div_tendsto_atBot_atTop_of_degree_gt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.atTop	—	comp_eq_zero_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass coeff_neg coeff_X_zero neg_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsSimpleRing.instNontrivial DivisionRing.isSimpleRing eval_comp eval_neg eval_X neg_neg Filter.Tendsto.comp abs_div_tendsto_atTop_atTop_of_degree_gt degree_comp_neg_X Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
abs_div_tendsto_atTop_atTop_of_degree_gt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	Filter.Tendsto.comp Filter.tendsto_abs_atTop_atTop div_tendsto_atTop_of_degree_gt Filter.tendsto_abs_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing div_tendsto_atBot_of_degree_gt LT.lt.le
abs_div_tendsto_atTop_of_degree_gt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	abs_div_tendsto_atTop_atTop_of_degree_gt
abs_isBoundedUnder_iff 📖	mathematical	—	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atTop abs NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField WithBot WithBot.instPreorder Nat.instPreorder degree WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	isBoundedUnder_abs_atTop_iff
abs_tendsto_atBot 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.atTop	—	eval_comp eval_neg eval_X neg_neg Filter.Tendsto.comp abs_tendsto_atTop degree_comp_neg_X Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
abs_tendsto_atBot_iff 📖	mathematical	—	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.atTop WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	—	not_le isBoundedUnder_abs_atBot_iff Filter.not_isBoundedUnder_of_tendsto_atTop instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Filter.atBot_neBot SemilatticeInf.instIsCodirectedOrder Nontrivial.to_nonempty abs_tendsto_atBot
abs_tendsto_atTop 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	le_total Filter.Tendsto.comp Filter.tendsto_abs_atTop_atTop tendsto_atTop_of_leadingCoeff_nonneg Filter.tendsto_abs_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing tendsto_atBot_of_leadingCoeff_nonpos
abs_tendsto_atTop_iff 📖	mathematical	—	Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	—	not_le isBoundedUnder_abs_atTop_iff Filter.not_isBoundedUnder_of_tendsto_atTop instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty abs_tendsto_atTop
div_tendsto_atBot_leadingCoeff_div_of_degree_eq 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing leadingCoeff	—	Asymptotics.IsEquivalent.tendsto_nhds Asymptotics.IsEquivalent.symm isEquivalent_atBot_div natDegree_eq_natDegree sub_self zpow_zero mul_one T5Space.toT1Space OrderTopology.t5Space Filter.atBot_neBot SemilatticeInf.instIsCodirectedOrder Nontrivial.to_nonempty IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
div_tendsto_atBot_of_degree_gt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing leadingCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	Filter.Tendsto eval Filter.atTop Filter.atBot	—	lt_of_le_of_ne div_ne_zero ne_zero_of_degree_gt leadingCoeff_eq_zero div_tendsto_atBot_of_degree_gt'
div_tendsto_atBot_of_degree_gt' 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing leadingCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	Filter.Tendsto eval Filter.atTop Filter.atBot	—	LT.lt.false div_zero Asymptotics.IsEquivalent.tendsto_atBot Asymptotics.IsEquivalent.symm isEquivalent_atTop_div Filter.Tendsto.const_mul_atTop_of_neg Filter.tendsto_zpow_atTop_atTop natDegree_lt_natDegree_iff
div_tendsto_atBot_zero_iff_degree_lt 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	degree_comp_neg_X comp_eq_zero_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass coeff_neg coeff_X_zero neg_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsSimpleRing.instNontrivial DivisionRing.isSimpleRing div_tendsto_atTop_zero_iff_degree_lt eval_comp eval_neg eval_X Filter.Tendsto.comp Filter.tendsto_neg_atTop_atBot IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing div_tendsto_atBot_zero_of_degree_lt
div_tendsto_atBot_zero_of_degree_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	eval_comp eval_neg eval_X neg_neg Filter.Tendsto.comp div_tendsto_atTop_zero_of_degree_lt degree_comp_neg_X Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
div_tendsto_atTop_leadingCoeff_div_of_degree_eq 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing leadingCoeff	—	Asymptotics.IsEquivalent.tendsto_nhds Asymptotics.IsEquivalent.symm isEquivalent_atTop_div sub_self zpow_zero mul_one T5Space.toT1Space OrderTopology.t5Space Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
div_tendsto_atTop_of_degree_gt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing leadingCoeff	Filter.Tendsto eval Filter.atTop	—	lt_of_le_of_ne div_ne_zero ne_zero_of_degree_gt leadingCoeff_eq_zero div_tendsto_atTop_of_degree_gt'
div_tendsto_atTop_of_degree_gt' 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing leadingCoeff	Filter.Tendsto eval Filter.atTop	—	LT.lt.false div_zero Asymptotics.IsEquivalent.tendsto_atTop Asymptotics.IsEquivalent.symm isEquivalent_atTop_div Filter.Tendsto.const_mul_atTop Filter.tendsto_zpow_atTop_atTop natDegree_lt_natDegree_iff
div_tendsto_atTop_zero_iff_degree_lt 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	div_eq_mul_inv NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass leadingCoeff_eq_zero degree_zero bot_lt_iff_ne_bot degree_eq_bot Asymptotics.IsEquivalent.tendsto_nhds isEquivalent_atTop_div tendsto_const_mul_zpow_atTop_nhds_iff degree_lt_degree zero_add sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono div_tendsto_atTop_zero_of_degree_lt
div_tendsto_atTop_zero_of_degree_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	eval_zero zero_div T5Space.toT1Space OrderTopology.t5Space Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Asymptotics.IsEquivalent.tendsto_nhds Asymptotics.IsEquivalent.symm isEquivalent_atTop_div MulZeroClass.mul_zero Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing tendsto_zpow_atTop_zero natDegree_lt_natDegree_iff
div_tendsto_leadingCoeff_div_of_degree_eq 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing leadingCoeff	—	div_tendsto_atTop_leadingCoeff_div_of_degree_eq
div_tendsto_zero_iff_degree_lt 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	div_tendsto_atTop_zero_iff_degree_lt
div_tendsto_zero_of_degree_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	div_tendsto_atTop_zero_of_degree_lt
eventually_atBot_not_isRoot 📖	mathematical	—	Filter.Eventually IsRoot DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.atBot_le_cofinite instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Set.Finite.compl_mem_cofinite finite_setOf_isRoot instIsDomain
eventually_atTop_not_isRoot 📖	mathematical	—	Filter.Eventually IsRoot DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.atTop_le_cofinite instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Set.Finite.compl_mem_cofinite finite_setOf_isRoot instIsDomain
eventually_no_roots 📖	mathematical	—	Filter.Eventually IsRoot DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eventually_atTop_not_isRoot
isBigO_atBot_of_degree_le 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Asymptotics.IsBigO NormedField.toNorm Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval	—	eval_comp eval_neg eval_X neg_neg Asymptotics.IsBigO.comp_tendsto isBigO_atTop_of_degree_le degree_comp_neg_X Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
isBigO_atTop_of_degree_le 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Asymptotics.IsBigO NormedField.toNorm Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval	—	eval_zero Asymptotics.isBigO_zero ne_zero_of_degree_ge_degree Filter.mem_of_superset eventually_atTop_not_isRoot le_iff_lt_or_eq Asymptotics.isBigO_of_div_tendsto_nhds div_tendsto_atTop_zero_of_degree_lt div_tendsto_atTop_leadingCoeff_div_of_degree_eq
isBigO_of_degree_le 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Asymptotics.IsBigO NormedField.toNorm Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval	—	isBigO_atTop_of_degree_le
isBoundedUnder_abs_atBot_iff 📖	mathematical	—	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atBot abs NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField WithBot WithBot.instPreorder Nat.instPreorder degree WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	Mathlib.Tactic.Contrapose.contrapose₁ Filter.not_isBoundedUnder_of_tendsto_atTop instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Filter.atBot_neBot SemilatticeInf.instIsCodirectedOrder Nontrivial.to_nonempty abs_tendsto_atBot Filter.eventually_map Filter.Eventually.of_forall le_of_eq trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv eq_C_of_degree_le_zero eval_C
isBoundedUnder_abs_atTop_iff 📖	mathematical	—	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atTop abs NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField WithBot WithBot.instPreorder Nat.instPreorder degree WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	Mathlib.Tactic.Contrapose.contrapose₁ Filter.not_isBoundedUnder_of_tendsto_atTop instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty abs_tendsto_atTop Filter.eventually_map Filter.Eventually.of_forall le_of_eq trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv eq_C_of_degree_le_zero eval_C
isEquivalent_atBot_div 📖	mathematical	—	Asymptotics.IsEquivalent NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing leadingCoeff DivInvMonoid.toZPow natDegree	—	eval_zero zero_div CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero zero_sub zpow_neg zpow_natCast MulZeroClass.zero_mul div_zero sub_zero Asymptotics.IsEquivalent.trans Asymptotics.IsEquivalent.symm Asymptotics.IsEquivalent.div isEquivalent_atBot_lead Filter.EventuallyEq.isEquivalent Filter.Eventually.mono Filter.eventually_lt_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing zpow_sub₀ LT.lt.ne
isEquivalent_atBot_lead 📖	mathematical	—	Asymptotics.IsEquivalent NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing leadingCoeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero natDegree	—	eval_comp eval_neg eval_X neg_neg comp_neg_X_leadingCoeff_eq mul_rotate natDegree_comp NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass natDegree_neg natDegree_X IsSimpleRing.instNontrivial DivisionRing.isSimpleRing mul_comm one_mul mul_neg mul_one Asymptotics.IsEquivalent.comp_tendsto isEquivalent_atTop_lead Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
isEquivalent_atTop_div 📖	mathematical	—	Asymptotics.IsEquivalent NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing leadingCoeff DivInvMonoid.toZPow natDegree	—	eval_zero zero_div CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero zero_sub zpow_neg zpow_natCast MulZeroClass.zero_mul div_zero sub_zero Asymptotics.IsEquivalent.trans Asymptotics.IsEquivalent.symm Asymptotics.IsEquivalent.div isEquivalent_atTop_lead Filter.EventuallyEq.isEquivalent Filter.Eventually.mono Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing zpow_sub₀ LT.lt.ne
isEquivalent_atTop_lead 📖	mathematical	—	Asymptotics.IsEquivalent NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing leadingCoeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero natDegree	—	eval_zero pow_zero mul_one eval_eq_sum_range Finset.sum_range_succ Asymptotics.IsLittleO.add_isEquivalent Asymptotics.IsLittleO.sum Asymptotics.IsLittleO.const_mul_left Asymptotics.IsLittleO.const_mul_right NormedDivisionRing.toNormMulClass leadingCoeff_eq_zero Asymptotics.isLittleO_pow_pow_atTop_of_lt Finset.mem_range Asymptotics.IsEquivalent.refl
isLittleO_atBot_of_degree_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Asymptotics.IsLittleO NormedField.toNorm Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval	—	eval_comp eval_neg eval_X neg_neg Asymptotics.IsLittleO.comp_tendsto isLittleO_atTop_of_degree_lt degree_comp_neg_X Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
isLittleO_atTop_of_degree_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	Asymptotics.IsLittleO NormedField.toNorm Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder eval	—	eval_zero ne_zero_of_degree_ge_degree LT.lt.le Filter.mem_of_superset eventually_atTop_not_isRoot Asymptotics.isLittleO_of_tendsto' div_tendsto_atTop_zero_of_degree_lt
tendsto_atBot_iff_leadingCoeff_nonpos 📖	mathematical	—	Filter.Tendsto eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atBot WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree Preorder.toLE leadingCoeff NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing degree_neg leadingCoeff_neg IsOrderedAddMonoid.toAddLeftMono
tendsto_atBot_of_leadingCoeff_nonpos 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder leadingCoeff NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	Filter.Tendsto eval Filter.atTop Filter.atBot	—	tendsto_atBot_iff_leadingCoeff_nonpos
tendsto_atTop_iff_leadingCoeff_nonneg 📖	mathematical	—	Filter.Tendsto eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree Preorder.toLE NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing leadingCoeff	—	Asymptotics.IsEquivalent.tendsto_atTop isEquivalent_atTop_lead natDegree_pos_iff_degree_pos pos_iff_ne_zero Nat.instCanonicallyOrderedAdd Filter.tendsto_const_mul_pow_atTop_iff LT.lt.le tendsto_atTop_of_leadingCoeff_nonneg
tendsto_atTop_of_leadingCoeff_nonneg 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing leadingCoeff	Filter.Tendsto eval Filter.atTop	—	Asymptotics.IsEquivalent.tendsto_atTop Asymptotics.IsEquivalent.symm isEquivalent_atTop_lead Filter.tendsto_const_mul_pow_atTop LT.lt.ne' natDegree_pos_iff_degree_pos LE.le.lt_of_ne' leadingCoeff_ne_zero ne_zero_of_degree_gt
tendsto_nhds_iff 📖	mathematical	—	Filter.Tendsto eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing leadingCoeff WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	Asymptotics.IsEquivalent.tendsto_nhds isEquivalent_atTop_lead trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv MulZeroClass.zero_mul T5Space.toT1Space OrderTopology.t5Space Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty IsSimpleRing.instNontrivial DivisionRing.isSimpleRing leadingCoeff_eq_zero natDegree_eq_zero_iff_degree_le_zero tendsto_const_mul_pow_nhds_iff Asymptotics.IsEquivalent.symm pow_zero mul_one tendsto_const_nhds

---

← Back to Index