Documentation Verification Report

TrailingCoefficient

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

Statistics

Metric	Count
Definitions `meromorphicTrailingCoeffAt`	1
Theorems `meromorphicTrailingCoeffAt_of_eq_nhdsNE`, `meromorphicTrailingCoeffAt_of_ne_zero`, `meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE`, `meromorphicTrailingCoeffAt_add_eq_add`, `meromorphicTrailingCoeffAt_add_eq_left_of_lt`, `meromorphicTrailingCoeffAt_mul`, `meromorphicTrailingCoeffAt_ne_zero`, `meromorphicTrailingCoeffAt_of_order_eq_top`, `meromorphicTrailingCoeffAt_pow`, `meromorphicTrailingCoeffAt_smul`, `meromorphicTrailingCoeffAt_zpow`, `tendsto_nhds_meromorphicTrailingCoeffAt`, `meromorphicTrailingCoeffAt_congr_nhdsNE`, `meromorphicTrailingCoeffAt_const`, `meromorphicTrailingCoeffAt_id_sub_const`, `meromorphicTrailingCoeffAt_inv`, `meromorphicTrailingCoeffAt_of_not_MeromorphicAt`, `meromorphicTrailingCoeffAt_prod`	18
Total	19

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicTrailingCoeffAt_of_eq_nhdsNE` 📖	mathematical	`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`	`meromorphicTrailingCoeffAt`	—	`MeromorphicAt.meromorphicAt_congr` `MeromorphicAt.fun_smul` `MeromorphicAt.fun_zpow` `MeromorphicAt.fun_sub` `MeromorphicAt.id` `MeromorphicAt.const` `meromorphicAt` `MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top` `Filter.EventuallyEq.eq_of_nhds` `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Continuous.continuousAt` `continuous_zero` `continuousAt` `PerfectSpace.not_isolated` `instPerfectSpace` `Filter.EventuallyEq.symm` `Filter.EventuallyEq.trans` `WithTop.untop₀_top` `zpow_zero` `one_smul` `meromorphicOrderAt_eq_top_iff` `meromorphicOrderAt_ne_top_iff` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `sub_eq_zero` `smul_eq_zero_iff_right` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `smul_sub`
`meromorphicTrailingCoeffAt_of_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`meromorphicTrailingCoeffAt`	—	`meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `Filter.univ_mem'` `zpow_zero` `one_smul`
`meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` 📖	mathematical	`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`	`meromorphicTrailingCoeffAt`	—	`MeromorphicAt.meromorphicAt_congr` `MeromorphicAt.fun_smul` `MeromorphicAt.fun_zpow` `MeromorphicAt.fun_sub` `MeromorphicAt.id` `MeromorphicAt.const` `meromorphicAt` `meromorphicOrderAt_eq_int_iff` `meromorphicTrailingCoeffAt_of_eq_nhdsNE`

MeromorphicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicTrailingCoeffAt_add_eq_add` 📖	mathematical	`MeromorphicAt` `meromorphicOrderAt`	`meromorphicTrailingCoeffAt` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`meromorphicTrailingCoeffAt_of_order_eq_top` `zero_add` `meromorphicTrailingCoeffAt_congr_nhdsNE` `Filter.mp_mem` `meromorphicOrderAt_eq_top_iff` `Filter.univ_mem'` `AddRightCancelSemigroup.toIsRightCancelAdd` `CanLift.prf` `WithTop.canLift` `meromorphicOrderAt_eq_int_iff` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `self_mem_nhdsWithin` `WithTop.coe_eq_coe` `smul_add` `AnalyticAt.add`
`meromorphicTrailingCoeffAt_add_eq_left_of_lt` 📖	mathematical	`MeromorphicAt` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `meromorphicOrderAt`	`meromorphicTrailingCoeffAt` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add_comm` `meromorphicAt_add_iff_meromorphicAt₁` `meromorphicTrailingCoeffAt_of_not_MeromorphicAt` `meromorphicTrailingCoeffAt_congr_nhdsNE` `Filter.mp_mem` `meromorphicOrderAt_eq_top_iff` `Filter.univ_mem'` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `CanLift.prf` `WithTop.canLift` `meromorphicOrderAt_eq_int_iff` `self_mem_nhdsWithin` `smul_add` `IsScalarTower.left` `zpow_add₀` `add_sub_cancel` `AnalyticAt.fun_add` `AnalyticAt.fun_smul` `NormedSpace.toIsBoundedSMul` `AnalyticAt.fun_zpow_nonneg` `AnalyticAt.fun_sub` `analyticAt_id` `analyticAt_const` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `LT.lt.le` `WithTop.coe_lt_coe` `sub_self` `zero_zpow` `sub_ne_zero` `ne_of_lt` `zero_smul` `add_zero` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `add_eq_left` `smul_eq_zero` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero`
`meromorphicTrailingCoeffAt_mul` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`meromorphicTrailingCoeffAt` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`meromorphicTrailingCoeffAt_smul`
`meromorphicTrailingCoeffAt_ne_zero` 📖	—	`MeromorphicAt`	—	—	`meromorphicOrderAt_ne_top_iff` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE`
`meromorphicTrailingCoeffAt_of_order_eq_top` 📖	mathematical	`meromorphicOrderAt` `Top.top` `WithTop` `WithTop.top`	`meromorphicTrailingCoeffAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`meromorphicTrailingCoeffAt_pow` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`meromorphicTrailingCoeffAt` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`zpow_natCast` `meromorphicTrailingCoeffAt_zpow`
`meromorphicTrailingCoeffAt_smul` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`meromorphicTrailingCoeffAt` `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`	—	`meromorphicTrailingCoeffAt_of_order_eq_top` `Int.instIsOrderedAddMonoid` `meromorphicOrderAt_smul` `top_add` `zero_smul` `add_top` `smul_zero` `meromorphicOrderAt_ne_top_iff` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `WithTop.untop₀_add` `zpow_add₀` `sub_ne_zero` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left`
`meromorphicTrailingCoeffAt_zpow` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`meromorphicTrailingCoeffAt` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow_zero` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero` `analyticAt_const` `ne_zero_of_eq_one` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `meromorphicTrailingCoeffAt_of_order_eq_top` `meromorphicOrderAt_zpow` `WithTop.mul_top` `zero_zpow` `meromorphicOrderAt_ne_top_iff` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `AnalyticAt.zpow` `Filter.mp_mem` `Filter.univ_mem'` `mul_comm` `mul_zpow` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `Int.instNontrivial` `WithTop.untop₀_mul`
`tendsto_nhds_meromorphicTrailingCoeffAt` 📖	mathematical	`MeromorphicAt`	`Filter.Tendsto` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `WithTop.untop₀` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Int.instNormedCommRing` `meromorphicOrderAt` `nhdsWithin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds` `meromorphicTrailingCoeffAt`	—	`WithTop.untop₀_top` `neg_zero` `zpow_zero` `one_smul` `meromorphicTrailingCoeffAt_of_order_eq_top` `Filter.Tendsto.congr'` `Filter.mp_mem` `meromorphicOrderAt_eq_top_iff` `Filter.univ_mem'` `Filter.EventuallyEq.refl` `ContinuousWithinAt.tendsto` `continuousWithinAt_const` `meromorphicOrderAt_ne_top_iff` `self_mem_nhdsWithin` `zpow_neg` `Pi.smul_apply'` `Pi.inv_apply` `Pi.pow_apply` `smul_assoc` `IsScalarTower.left` `smul_eq_mul` `zpow_add'` `neg_add_cancel` `AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE` `ContinuousAt.continuousWithinAt` `AnalyticAt.continuousAt`

(root)

Definitions

Name	Category	Theorems
`meromorphicTrailingCoeffAt` 📖	CompOp	27 math math: `MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add`, `AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE`, `MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top`, `MeromorphicOn.meromorphicTrailingCoeffAt_extract_zeros_poles`, `ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero`, `MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt`, `ValueDistribution.characteristic_sub_characteristic_inv_le`, `meromorphicTrailingCoeffAt_const`, `meromorphicTrailingCoeffAt_inv`, `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero`, `meromorphicTrailingCoeffAt_id_sub_const`, `meromorphicTrailingCoeffAt_congr_nhdsNE`, `Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational`, `MeromorphicOn.circleAverage_log_norm`, `MeromorphicAt.meromorphicTrailingCoeffAt_smul`, `Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt`, `Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const`, `MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles`, `meromorphicTrailingCoeffAt_prod`, `ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const`, `MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt`, `meromorphicTrailingCoeffAt_of_not_MeromorphicAt`, `MeromorphicAt.meromorphicTrailingCoeffAt_mul`, `Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational_off_support`, `MeromorphicAt.meromorphicTrailingCoeffAt_zpow`, `MeromorphicAt.meromorphicTrailingCoeffAt_pow`, `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicTrailingCoeffAt_congr_nhdsNE` 📖	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`	`meromorphicTrailingCoeffAt`	—	`meromorphicTrailingCoeffAt_of_not_MeromorphicAt` `Iff.not` `MeromorphicAt.meromorphicAt_congr` `MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top` `meromorphicOrderAt_congr` `meromorphicOrderAt_ne_top_iff` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm`
`meromorphicTrailingCoeffAt_const` 📖	mathematical	—	`meromorphicTrailingCoeffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top` `meromorphicOrderAt_eq_top_iff` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero` `analyticAt_const`
`meromorphicTrailingCoeffAt_id_sub_const` 📖	mathematical	—	`meromorphicTrailingCoeffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`sub_self` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `analyticAt_const` `one_ne_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `zpow_one` `mul_one` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero` `AnalyticAt.fun_sub` `analyticAt_id`
`meromorphicTrailingCoeffAt_inv` 📖	mathematical	—	`meromorphicTrailingCoeffAt` `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`	—	`MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top` `Int.instIsOrderedAddMonoid` `meromorphicOrderAt_inv` `LinearOrderedAddCommGroupWithTop.neg_top` `inv_zero` `Filter.mp_mem` `meromorphicOrderAt_ne_top_iff_eventually_ne_zero` `Filter.univ_mem'` `inv_mul_cancel₀` `mul_eq_one_iff_eq_inv₀` `MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero` `MeromorphicAt.meromorphicTrailingCoeffAt_mul` `MeromorphicAt.inv` `meromorphicTrailingCoeffAt_congr_nhdsNE` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE` `analyticAt_const` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `zpow_zero` `mul_one` `eventuallyEq_nhdsWithin_of_eqOn` `meromorphicTrailingCoeffAt_of_not_MeromorphicAt`
`meromorphicTrailingCoeffAt_of_not_MeromorphicAt` 📖	mathematical	`MeromorphicAt`	`meromorphicTrailingCoeffAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`meromorphicTrailingCoeffAt_prod` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`meromorphicTrailingCoeffAt` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`Finset.induction` `meromorphicTrailingCoeffAt_const` `Finset.prod_insert` `MeromorphicAt.meromorphicTrailingCoeffAt_mul` `MeromorphicAt.prod`

---

← Back to Index