Basic

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

Statistics

Metric	Count
Definitions `Meromorphic`, `MeromorphicAt`, `MeromorphicOn`	3
Theorems `meromorphicAt`, `meromorphicOn`, `countable_compl_analyticAt`, `measurable`, `add`, `congr_codiscrete`, `const`, `countable_compl_analyticAt`, `deriv`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_pow`, `fun_prod`, `fun_smul`, `fun_sub`, `fun_sum`, `fun_zpow`, `inv`, `iterated_deriv`, `measurable`, `meromorphicAt`, `meromorphicOn`, `mul`, `neg`, `pow`, `prod`, `smul`, `sub`, `sum`, `zpow`, `add`, `comp_analyticAt`, `const`, `deriv`, `div`, `eventually_analyticAt`, `eventually_continuousAt`, `eventually_eq_zero_or_eventually_ne_zero`, `fun_add`, `fun_deriv`, `fun_div`, `fun_inv`, `fun_iterated_deriv`, `fun_mul`, `fun_neg`, `fun_pow`, `fun_prod`, `fun_smul`, `fun_sub`, `fun_sum`, `fun_zpow`, `id`, `iff_eventuallyEq_zpow_smul_analyticAt`, `inv`, `inv_iff`, `iterated_deriv`, `meromorphicAt_add_iff_meromorphicAt₁`, `meromorphicAt_add_iff_meromorphicAt₂`, `meromorphicAt_congr`, `meromorphicAt_sub_iff_meromorphicAt₁`, `meromorphicAt_sub_iff_meromorphicAt₂`, `mul`, `neg`, `neg_iff`, `pow`, `prod`, `smul`, `sub`, `sum`, `update`, `update_iff`, `zpow`, `add`, `congr_codiscreteWithin`, `congr_codiscreteWithin_of_eqOn_compl`, `const`, `countable_compl_analyticAt`, `countable_compl_analyticAt_inter`, `deriv`, `div`, `eventually_codiscreteWithin_analyticAt`, `fun_add`, `fun_deriv`, `fun_div`, `fun_inv`, `fun_iterated_deriv`, `fun_mul`, `fun_neg`, `fun_pow`, `fun_prod`, `fun_smul`, `fun_sub`, `fun_sum`, `fun_zpow`, `id`, `inv`, `inv_iff`, `iterated_deriv`, `measurable`, `mono_set`, `mul`, `neg`, `neg_iff`, `pow`, `prod`, `smul`, `sub`, `sum`, `zpow`, `meromorphicAt_comp_iff_of_deriv_ne_zero`, `meromorphicAt_mul_iff_of_ne_zero`, `meromorphicAt_smul_iff_of_ne_zero`, `meromorphicOn_congr_codiscreteWithin`, `meromorphicOn_univ`, `meromorphic_congr_codiscrete`	119
Total	122

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicAt` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicAt`	—	`pow_zero` `one_smul`

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicOn` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicOn`	—	`AnalyticAt.meromorphicAt`

Meromorphic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Meromorphic`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeromorphicAt.add`
`congr_codiscrete` 📖	—	`Meromorphic` `Filter.EventuallyEq` `Filter.codiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField`	—	—	`meromorphicOn_univ` `MeromorphicOn.congr_codiscreteWithin` `Filter.eventuallyEq_of_mem` `isOpen_univ`
`const` 📖	mathematical	—	`Meromorphic`	—	`MeromorphicAt.const`
`countable_compl_analyticAt` 📖	mathematical	`Meromorphic`	`Set.Countable` `Compl.compl` `Set` `Set.instCompl` `setOf` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`Set.inter_univ` `MeromorphicOn.countable_compl_analyticAt_inter` `meromorphicOn`
`deriv` 📖	mathematical	`Meromorphic`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`MeromorphicAt.deriv`
`div` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`MeromorphicAt.div`
`fun_add` 📖	mathematical	`Meromorphic`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add`
`fun_div` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div`
`fun_inv` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`inv`
`fun_mul` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`mul`
`fun_neg` 📖	mathematical	`Meromorphic`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg`
`fun_pow` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`pow`
`fun_prod` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`Finset.prod_fn` `prod`
`fun_smul` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`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`	—	`smul`
`fun_sub` 📖	mathematical	`Meromorphic`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub`
`fun_sum` 📖	mathematical	`Meromorphic`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Finset.sum_fn` `sum`
`fun_zpow` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow`
`inv` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`MeromorphicAt.inv`
`iterated_deriv` 📖	mathematical	`Meromorphic`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`MeromorphicAt.iterated_deriv`
`measurable` 📖	mathematical	`Meromorphic`	`Measurable`	—	`countable_compl_analyticAt` `Set.Countable.to_subtype` `isOpen_analyticAt` `ContinuousAt.continuousWithinAt` `AnalyticAt.continuousAt` `Measurable.of_union_range_cover` `MeasurableEmbedding.subtype_coe` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `Set.Countable.measurableSet` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Subtype.range_coe_subtype` `Set.union_compl_self` `Set.instReflSubset` `Continuous.measurable` `Subtype.opensMeasurableSpace` `ContinuousOn.restrict` `measurable_of_countable` `Subtype.instMeasurableSingletonClass`
`meromorphicAt` 📖	mathematical	`Meromorphic`	`MeromorphicAt`	—	—
`meromorphicOn` 📖	mathematical	`Meromorphic`	`MeromorphicOn`	—	—
`mul` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`MeromorphicAt.mul`
`neg` 📖	mathematical	`Meromorphic`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeromorphicAt.neg`
`pow` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`MeromorphicAt.pow`
`prod` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`MeromorphicAt.prod`
`smul` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`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`	—	`MeromorphicAt.smul`
`sub` 📖	mathematical	`Meromorphic`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`MeromorphicAt.sub`
`sum` 📖	mathematical	`Meromorphic`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeromorphicAt.sum`
`zpow` 📖	mathematical	`Meromorphic` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`MeromorphicAt.zpow`

Meromorphic.MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable_compl_analyticAt` 📖	mathematical	`Meromorphic`	`Set.Countable` `Compl.compl` `Set` `Set.instCompl` `setOf` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`Meromorphic.countable_compl_analyticAt`
`measurable` 📖	mathematical	`Meromorphic`	`Measurable`	—	`Meromorphic.measurable`

MeromorphicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeromorphicAt`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`smul_add` `AnalyticAt.add` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `AnalyticAt.pow` `AnalyticAt.sub` `analyticAt_id` `analyticAt_const`
`comp_analyticAt` 📖	—	`MeromorphicAt` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	—	`congr` `const` `Filter.mp_mem` `nhdsWithin_le_nhds` `analyticOrderAt_eq_top` `Filter.univ_mem'` `WithTop.ne_top_iff_exists` `AnalyticAt.analyticOrderAt_eq_natCast` `AnalyticAt.fun_sub` `analyticAt_const` `AnalyticAt.fun_smul` `NormedSpace.toIsBoundedSMul` `AnalyticAt.fun_pow` `AnalyticAt.fun_inv` `AnalyticAt.comp'` `AnalyticAt.restrictScalars` `IsScalarTower.right` `AnalyticAt.congr` `Filter.Tendsto.eventually_ne` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousAt.tendsto` `AnalyticAt.continuousAt` `inv_pow` `inv_smul_eq_iff₀` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `SMulCommClass.smul_comm` `IsScalarTower.to_smulCommClass'` `smul_assoc` `pow_mul` `smul_pow` `Algebra.to_smulCommClass`
`const` 📖	mathematical	—	`MeromorphicAt`	—	`AnalyticAt.meromorphicAt` `analyticAt_const`
`deriv` 📖	mathematical	`MeromorphicAt`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`iff_eventuallyEq_zpow_smul_analyticAt` `Filter.mp_mem` `eventually_nhdsWithin_of_forall` `eventually_nhdsWithin_of_eventually_nhds` `AnalyticAt.eventually_analyticAt` `Filter.univ_mem'` `deriv_fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `DifferentiableAt.zpow` `DifferentiableAt.sub_const` `differentiableAt_id` `sub_ne_zero_of_ne` `AnalyticAt.differentiableAt` `add_comm` `deriv_comp_sub_const` `deriv_zpow'` `meromorphicAt_congr` `Filter.EventuallyEq.nhdsNE_deriv` `fun_add` `fun_smul` `fun_mul` `const` `fun_zpow` `fun_sub` `id` `AnalyticAt.meromorphicAt` `AnalyticAt.deriv`
`div` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`mul` `inv` `div_eq_mul_inv`
`eventually_analyticAt` 📖	mathematical	`MeromorphicAt`	`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` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Filter.Eventually.mp` `Filter.Eventually.filter_mono` `AnalyticAt.eventually_analyticAt` `eventually_nhdsWithin_iff` `Filter.Eventually.of_forall` `AnalyticAt.inv` `AnalyticAt.pow` `AnalyticAt.sub` `analyticAt_id` `analyticAt_const` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `sub_ne_zero_of_ne` `Set.mem_singleton_iff` `Set.mem_compl_iff` `AnalyticAt.congr` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `Filter.Eventually.mono` `eventually_ne_nhds` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `smul_smul` `inv_mul_cancel₀` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `one_smul`
`eventually_continuousAt` 📖	mathematical	`MeromorphicAt`	`Filter.Eventually` `ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`nhdsWithin_le_nhds` `AnalyticAt.eventually_continuousAt` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `ContinuousAt.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousAt.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousAt_id'` `continuousAt_const` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ContinuousAt.congr` `ContinuousAt.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `eventually_ne_nhds` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `smul_smul` `inv_mul_cancel₀` `one_smul`
`eventually_eq_zero_or_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`	—	`AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` `Filter.mp_mem` `self_mem_nhdsWithin` `nhdsWithin_le_nhds` `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_eq_zero` `Set.mem_singleton_iff` `Set.mem_compl_iff` `smul_ne_zero_iff`
`fun_add` 📖	mathematical	`MeromorphicAt`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add`
`fun_deriv` 📖	mathematical	`MeromorphicAt`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`deriv`
`fun_div` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div`
`fun_inv` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`inv`
`fun_iterated_deriv` 📖	mathematical	`MeromorphicAt`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`iterated_deriv`
`fun_mul` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`mul`
`fun_neg` 📖	mathematical	`MeromorphicAt`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg`
`fun_pow` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`pow`
`fun_prod` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`Finset.prod_apply` `prod`
`fun_smul` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`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`	—	`smul`
`fun_sub` 📖	mathematical	`MeromorphicAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub`
`fun_sum` 📖	mathematical	`MeromorphicAt`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Finset.sum_apply` `sum`
`fun_zpow` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow`
`id` 📖	mathematical	—	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`AnalyticAt.meromorphicAt` `analyticAt_id`
`iff_eventuallyEq_zpow_smul_analyticAt` 📖	mathematical	—	`MeromorphicAt` `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`	—	`eventually_nhdsWithin_iff` `Filter.univ_mem'` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.smul_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` `zpow_neg` `zpow_natCast` `mul_one` `inv_mul_cancel₀` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_ne_zero` `congr` `smul` `zpow` `sub` `id` `const` `AnalyticAt.meromorphicAt` `Filter.EventuallyEq.symm`
`inv` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`congr` `const` `eventuallyEq_nhdsWithin_iff` `Filter.mp_mem` `Filter.univ_mem'` `Pi.inv_apply` `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` `inv_zero` `AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff` `AnalyticAt.pow` `AnalyticAt.sub` `analyticAt_id` `analyticAt_const` `AnalyticAt.congr` `AnalyticAt.fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `AnalyticAt.inv` `ContinuousAt.eventually_ne` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `AnalyticAt.continuousAt` `eq_or_ne` `sub_self` `pow_succ` `MulZeroClass.mul_zero` `zero_smul` `pow_succ'` `SemigroupAction.mul_smul` `eq_inv_smul_iff₀` `SMulCommClass.smul_comm` `smulCommClass_self` `inv_smul_eq_iff₀` `smul_inv₀` `Algebra.to_smulCommClass` `IsScalarTower.right`
`inv_iff` 📖	mathematical	—	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`inv_inv` `inv`
`iterated_deriv` 📖	mathematical	`MeromorphicAt`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Function.iterate_succ'` `deriv`
`meromorphicAt_add_iff_meromorphicAt₁` 📖	mathematical	`MeromorphicAt`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add_sub_cancel_left` `sub` `add`
`meromorphicAt_add_iff_meromorphicAt₂` 📖	mathematical	`MeromorphicAt`	`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₁`
`meromorphicAt_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`	`MeromorphicAt`	—	`congr` `Filter.EventuallyEq.symm`
`meromorphicAt_sub_iff_meromorphicAt₁` 📖	mathematical	`MeromorphicAt`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_sub_cancel_left` `sub`
`meromorphicAt_sub_iff_meromorphicAt₂` 📖	mathematical	`MeromorphicAt`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_add_cancel` `add` `sub`
`mul` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`Algebra.mul_smul_comm` `Algebra.smul_mul_assoc` `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.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pf_right` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `AnalyticAt.mul`
`neg` 📖	mathematical	`MeromorphicAt`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg_smul` `one_smul` `smul` `const`
`neg_iff` 📖	mathematical	—	`MeromorphicAt` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg_neg` `neg`
`pow` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`pow_zero` `const` `pow_succ` `mul`
`prod` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`Finset.induction` `Finset.prod_empty` `AnalyticAt.meromorphicAt` `analyticAt_const` `Finset.prod_insert` `mul`
`smul` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`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`	—	`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.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pf_right` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left`
`sub` 📖	mathematical	`MeromorphicAt`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`sum` 📖	mathematical	`MeromorphicAt`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Finset.induction` `AnalyticAt.meromorphicAt` `analyticAt_const` `Finset.sum_insert` `add`
`update` 📖	mathematical	`MeromorphicAt`	`Function.update`	—	`update_iff`
`update_iff` 📖	mathematical	—	`MeromorphicAt` `Function.update`	—	`meromorphicAt_congr` `Function.update_eventuallyEq_nhdsNE` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace`
`zpow` 📖	mathematical	`MeromorphicAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow_natCast` `pow` `zpow_negSucc`

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeromorphicOn`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeromorphicAt.add`
`congr_codiscreteWithin` 📖	—	`MeromorphicOn` `Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `IsOpen`	—	—	`MeromorphicAt.congr` `mem_nhdsWithin` `Set.inter_subset_left` `Filter.mp_mem` `Filter.univ_mem'`
`congr_codiscreteWithin_of_eqOn_compl` 📖	—	`MeromorphicOn` `Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Set.EqOn` `Compl.compl` `Set` `Set.instCompl`	—	—	`MeromorphicAt.congr` `Filter.mp_mem` `Filter.univ_mem'`
`const` 📖	mathematical	—	`MeromorphicOn`	—	`MeromorphicAt.const`
`countable_compl_analyticAt` 📖	mathematical	`Meromorphic`	`Set.Countable` `Compl.compl` `Set` `Set.instCompl` `setOf` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`Meromorphic.countable_compl_analyticAt`
`countable_compl_analyticAt_inter` 📖	mathematical	`MeromorphicOn`	`Set.Countable` `Set` `Set.instInter` `Compl.compl` `Set.instCompl` `setOf` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`IsLindelof.countable_of_isDiscrete` `HereditarilyLindelofSpace.isLindelof` `SecondCountableTopology.toHereditarilyLindelof` `isDiscrete_of_codiscreteWithin` `compl_compl` `eventually_codiscreteWithin_analyticAt`
`deriv` 📖	mathematical	`MeromorphicOn`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`MeromorphicAt.deriv`
`div` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`MeromorphicAt.div`
`eventually_codiscreteWithin_analyticAt` 📖	mathematical	`MeromorphicOn`	`Filter.Eventually` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`Filter.eventually_iff` `mem_codiscreteWithin` `Filter.disjoint_principal_right` `Filter.mem_of_superset` `MeromorphicAt.eventually_analyticAt`
`fun_add` 📖	mathematical	`MeromorphicOn`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add`
`fun_deriv` 📖	mathematical	`MeromorphicOn`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`deriv`
`fun_div` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div`
`fun_inv` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`inv`
`fun_iterated_deriv` 📖	mathematical	`MeromorphicOn`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`iterated_deriv`
`fun_mul` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`mul`
`fun_neg` 📖	mathematical	`MeromorphicOn`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg`
`fun_pow` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`pow`
`fun_prod` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`MeromorphicAt.fun_prod`
`fun_smul` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`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`	—	`smul`
`fun_sub` 📖	mathematical	`MeromorphicOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub`
`fun_sum` 📖	mathematical	`MeromorphicOn`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeromorphicAt.fun_sum`
`fun_zpow` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`zpow`
`id` 📖	mathematical	—	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`MeromorphicAt.id`
`inv` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`MeromorphicAt.inv`
`inv_iff` 📖	mathematical	—	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`inv_inv` `inv`
`iterated_deriv` 📖	mathematical	`MeromorphicOn`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`MeromorphicAt.iterated_deriv`
`measurable` 📖	mathematical	`Meromorphic`	`Measurable`	—	`Meromorphic.measurable`
`mono_set` 📖	—	`MeromorphicOn` `Set` `Set.instHasSubset`	—	—	—
`mul` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`MeromorphicAt.mul`
`neg` 📖	mathematical	`MeromorphicOn`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeromorphicAt.neg`
`neg_iff` 📖	mathematical	—	`MeromorphicOn` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg_neg` `neg`
`pow` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`MeromorphicAt.pow`
`prod` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField`	—	`MeromorphicAt.prod`
`smul` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`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`	—	`MeromorphicAt.smul`
`sub` 📖	mathematical	`MeromorphicOn`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`MeromorphicAt.sub`
`sum` 📖	mathematical	`MeromorphicOn`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeromorphicAt.sum`
`zpow` 📖	mathematical	`MeromorphicOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toNormedSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Pi.instPow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`MeromorphicAt.zpow`

(root)

Definitions

Name	Category	Theorems
`Meromorphic` 📖	MathDef	7 math math: `Complex.meromorphic_digamma`, `meromorphicOn_univ`, `PeriodPair.meromorphic_derivWeierstrassP`, `Meromorphic.const`, `meromorphic_congr_codiscrete`, `PeriodPair.meromorphic_weierstrassP`, `Meromorphic.Gamma`
`MeromorphicAt` 📖	MathDef	15 math math: `MeromorphicAt.inv_iff`, `MeromorphicAt.const`, `MeromorphicAt.neg_iff`, `MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt`, `meromorphicNFAt_iff_analyticAt_or`, `MeromorphicAt.meromorphicAt_congr`, `MeromorphicAt.id`, `MeromorphicNFAt.meromorphicAt`, `MeromorphicAt.update_iff`, `Meromorphic.meromorphicAt`, `meromorphicAt_comp_iff_of_deriv_ne_zero`, `meromorphicAt_mul_iff_of_ne_zero`, `meromorphicAt_of_meromorphicOrderAt_ne_zero`, `meromorphicAt_smul_iff_of_ne_zero`, `AnalyticAt.meromorphicAt`
`MeromorphicOn` 📖	MathDef	11 math math: `meromorphicOn_univ`, `MeromorphicOn.id`, `meromorphicOn_congr_codiscreteWithin`, `Meromorphic.meromorphicOn`, `MeromorphicOn.const`, `MeromorphicOn.inv_iff`, `MeromorphicOn.neg_iff`, `MeromorphicNFOn.meromorphicOn`, `MeromorphicOn.divisor_def`, `MeromorphicOn.Gamma`, `AnalyticOnNhd.meromorphicOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicAt_comp_iff_of_deriv_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicAt`	—	`AnalyticAt.hasStrictDerivAt` `AnalyticAt.analyticAt_localInverse` `HasStrictFDerivAt.localInverse_apply_image` `HasStrictDerivAt.hasStrictFDerivAt_equiv` `MeromorphicAt.congr` `MeromorphicAt.comp_analyticAt` `IsScalarTower.left` `Filter.EventuallyEq.filter_mono` `Filter.EventuallyEq.fun_comp` `HasStrictDerivAt.eventually_right_inverse` `nhdsWithin_le_nhds`
`meromorphicAt_mul_iff_of_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicAt` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`meromorphicAt_smul_iff_of_ne_zero`
`meromorphicAt_smul_iff_of_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicAt` `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`	—	`MeromorphicAt.congr` `MeromorphicAt.smul` `AnalyticAt.meromorphicAt` `AnalyticAt.inv` `Filter.mp_mem` `Filter.Tendsto.eventually_ne` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.Tendsto.mono_left` `AnalyticAt.continuousAt` `nhdsWithin_le_nhds` `Filter.univ_mem'` `inv_smul_smul₀`
`meromorphicOn_congr_codiscreteWithin` 📖	mathematical	`Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `IsOpen`	`MeromorphicOn`	—	`MeromorphicOn.congr_codiscreteWithin` `Filter.EventuallyEq.symm`
`meromorphicOn_univ` 📖	mathematical	—	`MeromorphicOn` `Set.univ` `Meromorphic`	—	—
`meromorphic_congr_codiscrete` 📖	mathematical	`Filter.EventuallyEq` `Filter.codiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField`	`Meromorphic`	—	`Meromorphic.congr_codiscrete` `Filter.EventuallyEq.symm`

---

← Back to Index