Documentation Verification Report

FactorizedRational

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

Statistics

Metric	Count
Definitions	0
Theorems `analyticAt`, `divisor`, `extractFactor`, `finprod_eq_fun`, `log_norm_meromorphicTrailingCoeffAt`, `meromorphicNFOn`, `meromorphicNFOn_univ`, `meromorphicOrderAt_eq`, `meromorphicOrderAt_ne_top`, `meromorphicTrailingCoeffAt_factorizedRational`, `meromorphicTrailingCoeffAt_factorizedRational_off_support`, `mulSupport`, `ne_zero`, `extract_zeros_poles`, `extract_zeros_poles_log`, `log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles`, `meromorphicTrailingCoeffAt_extract_zeros_poles`	17
Total	17

Function.FactorizedRational

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	—	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`analyticAt_finprod` `AnalyticAt.fun_zpow_nonneg` `AnalyticAt.fun_sub` `analyticAt_id` `analyticAt_const` `AnalyticAt.fun_zpow` `sub_ne_zero`
`divisor` 📖	mathematical	—	`MeromorphicOn.divisor` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike`	—	`Function.locallyFinsuppWithin.ext` `MeromorphicOn.divisor_apply` `MeromorphicNFOn.meromorphicOn` `meromorphicNFOn` `meromorphicOrderAt_eq` `Function.locallyFinsuppWithin.apply_eq_zero_of_notMem`
`extractFactor` 📖	mathematical	—	`finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `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` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Function.update`	—	`zpow_zero` `Function.eq_update_self_iff` `one_mul` `mulSupport` `Set.Finite.coe_toFinset` `Set.instReflSubset` `finprod_eq_prod_of_mulSupport_subset` `Finset.mul_prod_erase` `Function.update_self` `Finset.coe_erase` `Function.update_of_ne` `Finset.prod_congr`
`finprod_eq_fun` 📖	mathematical	—	`finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `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`	—	`finprod_eq_prod_of_mulSupport_subset` `mulSupport` `Set.Finite.coe_toFinset` `Set.instReflSubset` `Mathlib.Tactic.Contrapose.contrapose₁` `zpow_zero` `Finset.prod_apply` `Finset.prod_congr`
`log_norm_meromorphicTrailingCoeffAt` 📖	mathematical	—	`Real.log` `Norm.norm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `meromorphicTrailingCoeffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `finsum` `Real` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast`	—	`meromorphicTrailingCoeffAt_factorizedRational` `finprod_eq_prod_of_mulSupport_subset` `sub_self` `Function.update_self` `zpow_zero` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `NeZero.one` `Real.instNontrivial` `norm_zpow` `norm_prod` `NormedDivisionRing.toNormMulClass` `Real.log_prod` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.Finite.coe_toFinset` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `Int.cast_zero` `finsum_eq_sum_of_support_subset` `Finset.sum_congr` `Real.log_zpow` `norm_zero` `Real.log_zero` `MulZeroClass.mul_zero` `Function.update_of_ne`
`meromorphicNFOn` 📖	mathematical	—	`MeromorphicNFOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`meromorphicNFOn_univ`
`meromorphicNFOn_univ` 📖	mathematical	—	`MeromorphicNFOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set.univ`	—	`extractFactor` `Function.update_self` `finprod_of_infinite_mulSupport` `mulSupport` `AnalyticOnNhd.meromorphicNFOn` `analyticOnNhd_const`
`meromorphicOrderAt_eq` 📖	mathematical	—	`meromorphicOrderAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `WithTop.some`	—	`meromorphicOrderAt_eq_int_iff` `MeromorphicNFOn.meromorphicOn` `meromorphicNFOn_univ` `Set.mem_univ` `Function.update_self` `Filter.univ_mem'` `extractFactor`
`meromorphicOrderAt_ne_top` 📖	—	—	—	—	`meromorphicOrderAt_eq` `finprod_of_infinite_mulSupport` `mulSupport` `meromorphicOrderAt_const_ofNat` `Nat.cast_one` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Int.instIsOrderedAddMonoid`
`meromorphicTrailingCoeffAt_factorizedRational` 📖	mathematical	—	`meromorphicTrailingCoeffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Function.update`	—	`mulSupport` `Set.Finite.coe_toFinset` `Set.instReflSubset` `finprod_eq_prod_of_mulSupport_subset` `meromorphicTrailingCoeffAt_prod` `MeromorphicAt.zpow` `MeromorphicAt.fun_sub` `MeromorphicAt.id` `MeromorphicAt.const` `Finset.prod_congr` `MeromorphicAt.meromorphicTrailingCoeffAt_zpow` `meromorphicTrailingCoeffAt_id_sub_const` `one_zpow` `sub_self` `Function.update_self` `zpow_zero`
`meromorphicTrailingCoeffAt_factorizedRational_off_support` 📖	mathematical	`Set` `Set.instMembership` `Function.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing`	`meromorphicTrailingCoeffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`meromorphicTrailingCoeffAt_factorizedRational` `finprod_eq_prod_of_mulSupport_subset` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.Finite.coe_toFinset` `zpow_zero` `Finset.prod_congr` `Function.update_of_ne`
`mulSupport` 📖	mathematical	—	`Function.mulSupport` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Function.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Int.instNormedCommRing`	—	`Set.ext` `zpow_zero` `sub_self`
`ne_zero` 📖	—	—	—	—	`finprod_eq_prod` `Finset.prod_apply` `Finset.prod_ne_zero_iff` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `zpow_zero` `finprod_of_infinite_mulSupport` `NeZero.one`

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extract_zeros_poles` 📖	mathematical	`MeromorphicOn`	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Pi.smul'` `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` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `Function.locallyFinsuppWithin` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `divisor`	—	`MeromorphicNFOn.meromorphicOn` `Function.FactorizedRational.meromorphicNFOn` `meromorphicNFOn_toMeromorphicNFOn` `MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd` `divisor_of_toMeromorphicNFOn` `smul` `inv` `divisor_smul` `Int.instIsOrderedAddMonoid` `meromorphicOrderAt_inv` `Function.FactorizedRational.meromorphicOrderAt_ne_top` `divisor_inv` `Function.FactorizedRational.divisor` `neg_add_cancel` `le_refl` `MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff` `meromorphicOrderAt_congr` `Filter.EventuallyEq.symm` `toMeromorphicNFOn_eq_self_on_nhdsNE` `meromorphicOrderAt_smul` `MeromorphicAt.inv` `Function.FactorizedRational.meromorphicOrderAt_eq` `divisor_apply` `CanLift.prf` `WithTop.canLift` `WithTop.untop₀_coe` `WithTop.LinearOrderedAddCommGroup.coe_neg` `WithTop.coe_add` `Filter.mp_mem` `Filter.self_mem_codiscreteWithin` `meromorphicNFAt_mem_codiscreteWithin` `Function.locallyFinsuppWithin.eq_zero_codiscreteWithin` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.univ_mem'` `toMeromorphicNFOn_eq_toMeromorphicNFAt` `toMeromorphicNFAt_eq_self` `smul_assoc` `IsScalarTower.left` `smul_eq_mul` `mul_inv_cancel₀` `Function.FactorizedRational.meromorphicNFOn_univ` `Pi.zero_apply` `WithTop.coe_zero` `one_smul`
`extract_zeros_poles_log` 📖	mathematical	`Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Pi.smul'` `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` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `DFunLike.coe` `Function.locallyFinsuppWithin` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike`	`Real` `Real.log` `Norm.norm` `NormedAddCommGroup.toNorm` `Pi.instAdd` `Real.instAdd` `finsum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `NormedField.toNorm`	—	`Set.ext` `not_iff_not` `NormedField.exists_one_lt_norm` `add_sub_cancel_right` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `norm_zero` `Int.cast_zero` `MulZeroClass.zero_mul` `Filter.mp_mem` `Filter.self_mem_codiscreteWithin` `Function.locallyFinsuppWithin.eq_zero_codiscreteWithin` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.univ_mem'` `finprod_eq_prod_of_mulSupport_subset` `Function.FactorizedRational.mulSupport` `Set.Finite.coe_toFinset` `Set.instReflSubset` `finsum_eq_sum_of_support_subset` `zpow_eq_zero_iff` `Function.mem_support` `Set.Finite.mem_toFinset` `norm_eq_zero` `sub_eq_zero` `Pi.zero_apply` `Finset.prod_apply` `Finset.prod_congr` `norm_smul` `NormedSpace.toNormSMulClass` `norm_prod` `NormedDivisionRing.to_normOneClass` `norm_zpow` `Real.log_mul` `Finset.prod_ne_zero_iff` `Real.instNontrivial` `Real.log_prod` `Finset.sum_congr` `Real.log_zpow` `Finset.sum_apply` `finsum_of_infinite_support` `finprod_of_infinite_mulSupport` `one_smul` `zero_add`
`log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles` 📖	mathematical	`Set` `Set.instMembership` `MeromorphicAt` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Pi.smul'` `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` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Real.log` `Norm.norm` `NormedAddCommGroup.toNorm` `meromorphicTrailingCoeffAt` `Real` `Real.instAdd` `finsum` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `NormedField.toNorm`	—	`meromorphicTrailingCoeffAt_congr_nhdsNE` `MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin` `MeromorphicAt.smul` `MeromorphicNFOn.meromorphicOn` `Function.FactorizedRational.meromorphicNFOn` `AnalyticAt.meromorphicAt` `MeromorphicAt.meromorphicTrailingCoeffAt_smul` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero` `norm_smul` `NormedSpace.toNormSMulClass` `Real.log_mul` `MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero` `Function.FactorizedRational.meromorphicOrderAt_ne_top` `Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt`
`meromorphicTrailingCoeffAt_extract_zeros_poles` 📖	mathematical	`Set` `Set.instMembership` `MeromorphicAt` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Pi.smul'` `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` `finprod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`meromorphicTrailingCoeffAt` `Function.update`	—	`MeromorphicNFOn.meromorphicOn` `Function.FactorizedRational.meromorphicNFOn` `meromorphicTrailingCoeffAt_congr_nhdsNE` `MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin` `MeromorphicAt.smul` `AnalyticAt.meromorphicAt` `MeromorphicAt.meromorphicTrailingCoeffAt_smul` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero` `Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational`

---

← Back to Index