NormalForm

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

Statistics

Metric	Count
Definitions `MeromorphicNFAt`, `MeromorphicNFOn`, `toMeromorphicNFAt`, `toMeromorphicNFOn`	4
Theorems `meromorphicNFAt`, `meromorphicNFOn`, `eqOn_compl_singleton_toMeromorphicNFAt`, `eq_nhdsNE_toMeromorphicNFAt`, `eventuallyEq_nhdsNE_iff_eventuallyEq_nhds`, `inv`, `meromorphicAt`, `meromorphicOrderAt_eq_zero_iff`, `meromorphicOrderAt_nonneg_iff_analyticAt`, `smul_analytic`, `divisor_nonneg_iff_analyticOnNhd`, `meromorphicOn`, `zero_set_eq_divisor_support`, `divisor_of_toMeromorphicNFOn`, `meromorphicNFAt_mem_codiscreteWithin`, `toMeromorphicNFOn_eq_self_on_nhdsNE`, `meromorphicNFAt_congr`, `meromorphicNFAt_iff_analyticAt_or`, `meromorphicNFAt_inv`, `meromorphicNFAt_mul_iff_left`, `meromorphicNFAt_mul_iff_right`, `meromorphicNFAt_smul_iff_right_of_analyticAt`, `meromorphicNFAt_toMeromorphicNFAt`, `meromorphicNFOn_inv`, `meromorphicNFOn_mul_iff_left_of_analyticOnNhd`, `meromorphicNFOn_mul_iff_right_of_analyticOnNhd`, `meromorphicNFOn_smul_iff_right_of_analyticOnNhd`, `meromorphicNFOn_toMeromorphicNFOn`, `meromorphicOrderAt_toMeromorphicNFOn`, `toMeromorphicNFAt_eq_self`, `toMeromorphicNFAt_of_not_meromorphicAt`, `toMeromorphicNFOn_eqOn_codiscrete`, `toMeromorphicNFOn_eq_self`, `toMeromorphicNFOn_eq_self_on_compl`, `toMeromorphicNFOn_eq_toMeromorphicNFAt`, `toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds`, `toMeromorphicNFOn_of_not_meromorphicOn`	37
Total	41

AnalyticAt

Theorems

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

AnalyticOnNhd

Theorems

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

MeromorphicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqOn_compl_singleton_toMeromorphicNFAt` 📖	mathematical	`MeromorphicAt`	`Set.EqOn` `toMeromorphicNFAt` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Function.update.congr_simp` `Function.update_of_ne`
`eq_nhdsNE_toMeromorphicNFAt` 📖	mathematical	`MeromorphicAt`	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `toMeromorphicNFAt`	—	`eventually_nhdsWithin_of_forall` `eqOn_compl_singleton_toMeromorphicNFAt`

MeromorphicNFAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyEq_nhdsNE_iff_eventuallyEq_nhds` 📖	mathematical	`MeromorphicNFAt`	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`meromorphicOrderAt_congr` `AnalyticAt.continuousAt` `meromorphicOrderAt_nonneg_iff_analyticAt` `le_of_eq` `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `PerfectSpace.not_isolated` `instPerfectSpace` `eventuallyEq_nhds_of_eventuallyEq_nhdsNE` `meromorphicOrderAt_eq_zero_iff` `Filter.EventuallyEq.filter_mono` `nhdsWithin_le_nhds`
`inv` 📖	mathematical	`MeromorphicNFAt` `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`	—	`Filter.mp_mem` `Filter.univ_mem'` `inv_zero` `AnalyticAt.inv` `mul_inv_rev` `zpow_neg` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_inv_one` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`meromorphicAt` 📖	mathematical	`MeromorphicNFAt`	`MeromorphicAt`	—	`meromorphicNFAt_iff_analyticAt_or` `AnalyticAt.meromorphicAt`
`meromorphicOrderAt_eq_zero_iff` 📖	mathematical	`MeromorphicNFAt`	`meromorphicOrderAt` `WithTop` `WithTop.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing`	—	`meromorphicOrderAt_nonneg_iff_analyticAt` `le_of_eq` `AnalyticAt.analyticOrderAt_eq_zero` `ENat.map_natCast_eq_zero` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero` `AnalyticAt.meromorphicOrderAt_eq` `Filter.EventuallyEq.eq_of_nhds` `sub_self` `zero_zpow` `zero_smul` `meromorphicOrderAt_eq_int_iff` `meromorphicAt` `zpow_zero` `Filter.EventuallyEq.filter_mono` `nhdsWithin_le_nhds`
`meromorphicOrderAt_nonneg_iff_analyticAt` 📖	mathematical	`MeromorphicNFAt`	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `WithTop.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `meromorphicOrderAt` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`meromorphicNFAt_iff_analyticAt_or` `lt_irrefl` `lt_of_le_of_lt` `AnalyticAt.meromorphicOrderAt_eq` `Int.instAddLeftMono` `Int.instZeroLEOneClass`
`smul_analytic` 📖	mathematical	`MeromorphicNFAt` `AnalyticAt` `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`	—	`Filter.mp_mem` `Filter.univ_mem'` `smul_zero` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `smul_ne_zero` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `SMulCommClass.smul_comm` `smulCommClass_self`

MeromorphicNFOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divisor_nonneg_iff_analyticOnNhd` 📖	mathematical	`MeromorphicNFOn`	`Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instLE` `Function.locallyFinsuppWithin.instZero` `Int.instAddCommGroup` `MeromorphicOn.divisor` `AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedField.toNormedSpace`	—	`MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt` `MeromorphicOn.divisor_apply` `meromorphicOn` `Function.locallyFinsuppWithin.apply_eq_zero_of_notMem`
`meromorphicOn` 📖	mathematical	`MeromorphicNFOn`	`MeromorphicOn`	—	`MeromorphicNFAt.meromorphicAt`
`zero_set_eq_divisor_support` 📖	mathematical	`MeromorphicNFOn`	`Set` `Set.instInter` `Set.preimage` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Function.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Function.locallyFinsuppWithin.instFunLike` `MeromorphicOn.divisor`	—	`Set.ext` `MeromorphicOn.divisor_apply` `meromorphicOn` `MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff` `Function.locallyFinsuppWithin.supportWithinDomain` `Set.mem_preimage` `Set.mem_singleton_iff` `Iff.not`

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divisor_of_toMeromorphicNFOn` 📖	mathematical	`MeromorphicOn`	`divisor` `toMeromorphicNFOn`	—	`Function.locallyFinsuppWithin.ext` `divisor_apply` `MeromorphicNFOn.meromorphicOn` `meromorphicNFOn_toMeromorphicNFOn` `meromorphicOrderAt_toMeromorphicNFOn` `Function.locallyFinsuppWithin.apply_eq_zero_of_notMem`
`meromorphicNFAt_mem_codiscreteWithin` 📖	mathematical	`MeromorphicOn`	`Set` `Filter` `Filter.instMembership` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `setOf` `MeromorphicNFAt`	—	`Filter.mp_mem` `analyticAt_mem_codiscreteWithin` `Filter.univ_mem'` `AnalyticAt.meromorphicNFAt`
`toMeromorphicNFOn_eq_self_on_nhdsNE` 📖	mathematical	`MeromorphicOn` `Set` `Set.instMembership`	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `toMeromorphicNFOn`	—	`Filter.mp_mem` `eventually_analyticAt_or_mem_compl` `Filter.univ_mem'` `toMeromorphicNFAt_eq_self` `AnalyticAt.meromorphicNFAt`

(root)

Definitions

Name	Category	Theorems
`MeromorphicNFAt` 📖	MathDef	10 math math: `meromorphicNFAt_toMeromorphicNFAt`, `meromorphicNFAt_mul_iff_left`, `meromorphicNFAt_inv`, `MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin`, `meromorphicNFAt_iff_analyticAt_or`, `toMeromorphicNFAt_eq_self`, `meromorphicNFAt_congr`, `AnalyticAt.meromorphicNFAt`, `meromorphicNFAt_smul_iff_right_of_analyticAt`, `meromorphicNFAt_mul_iff_right`
`MeromorphicNFOn` 📖	MathDef	10 math math: `meromorphicNFOn_mul_iff_right_of_analyticOnNhd`, `meromorphicNFOn_smul_iff_right_of_analyticOnNhd`, `Function.FactorizedRational.meromorphicNFOn_univ`, `meromorphicNFOn_mul_iff_left_of_analyticOnNhd`, `meromorphicNFOn_inv`, `meromorphicNFOn_toMeromorphicNFOn`, `AnalyticOnNhd.meromorphicNFOn`, `MeromorphicNFOn.Gamma`, `Function.FactorizedRational.meromorphicNFOn`, `toMeromorphicNFOn_eq_self`
`toMeromorphicNFAt` 📖	CompOp	7 math math: `meromorphicNFAt_toMeromorphicNFAt`, `toMeromorphicNFOn_eq_toMeromorphicNFAt`, `MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt`, `toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds`, `toMeromorphicNFAt_eq_self`, `MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt`, `toMeromorphicNFAt_of_not_meromorphicAt`
`toMeromorphicNFOn` 📖	CompOp	10 math math: `MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE`, `toMeromorphicNFOn_eq_toMeromorphicNFAt`, `meromorphicOrderAt_toMeromorphicNFOn`, `toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds`, `toMeromorphicNFOn_of_not_meromorphicOn`, `meromorphicNFOn_toMeromorphicNFOn`, `MeromorphicOn.divisor_of_toMeromorphicNFOn`, `toMeromorphicNFOn_eq_self_on_compl`, `toMeromorphicNFOn_eq_self`, `toMeromorphicNFOn_eqOn_codiscrete`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`meromorphicNFAt_congr` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField`	`MeromorphicNFAt`	—	`Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm`
`meromorphicNFAt_iff_analyticAt_or` 📖	mathematical	—	`MeromorphicNFAt` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `MeromorphicAt` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `meromorphicOrderAt` `WithTop.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Int.instNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`analyticAt_congr` `analyticAt_const` `MeromorphicAt.congr` `MeromorphicAt.smul` `MeromorphicAt.zpow` `MeromorphicAt.fun_sub` `MeromorphicAt.id` `MeromorphicAt.const` `AnalyticAt.meromorphicAt` `Filter.EventuallyEq.symm` `Filter.EventuallyEq.filter_mono` `nhdsWithin_le_nhds` `meromorphicOrderAt_eq_int_iff` `eventually_nhdsWithin_of_eventually_nhds` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `AnalyticAt.zpow_nonneg` `AnalyticAt.fun_sub` `analyticAt_id` `WithTop.coe_lt_zero` `Filter.EventuallyEq.eq_of_nhds` `sub_self` `zero_zpow` `LT.lt.ne` `zero_smul` `analyticOrderAt_eq_top` `AnalyticAt.analyticOrderAt_eq_natCast` `ENat.coe_toNat_eq_self` `zpow_natCast` `CanLift.prf` `WithTop.canLift` `LT.lt.ne_top` `Filter.mp_mem` `eventually_nhdsWithin_iff` `Filter.univ_mem'` `smul_eq_zero_of_left`
`meromorphicNFAt_inv` 📖	mathematical	—	`MeromorphicNFAt` `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`	—	`inv_inv` `MeromorphicNFAt.inv`
`meromorphicNFAt_mul_iff_left` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicNFAt` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`mul_comm` `smul_eq_mul` `meromorphicNFAt_smul_iff_right_of_analyticAt`
`meromorphicNFAt_mul_iff_right` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicNFAt` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`meromorphicNFAt_smul_iff_right_of_analyticAt`
`meromorphicNFAt_smul_iff_right_of_analyticAt` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicNFAt` `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`	—	`Filter.mp_mem` `ContinuousAt.preimage_mem_nhds` `AnalyticAt.continuousAt` `compl_singleton_mem_nhds_iff` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.univ_mem'` `inv_smul_smul₀` `Set.mem_singleton_iff` `Set.mem_preimage` `Set.mem_compl_iff` `Set.preimage_compl` `meromorphicNFAt_congr` `MeromorphicNFAt.smul_analytic` `AnalyticAt.inv` `inv_ne_zero`
`meromorphicNFAt_toMeromorphicNFAt` 📖	mathematical	—	`MeromorphicNFAt` `toMeromorphicNFAt`	—	`eventuallyEq_nhds_of_eventuallyEq_nhdsNE` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt` `meromorphicOrderAt_eq_top_iff` `Function.update.congr_simp` `Int.instIsOrderedAddMonoid` `Function.update_self` `AnalyticAt.meromorphicNFAt` `analyticAt_congr` `analyticAt_const` `CanLift.prf` `WithTop.canLift` `meromorphicOrderAt_eq_int_iff` `sub_self` `Filter.EventuallyEq.eq_of_nhds` `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `AnalyticAt.continuousAt` `ContinuousAt.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `PerfectSpace.not_isolated` `instPerfectSpace` `Filter.mp_mem` `Filter.univ_mem'` `zpow_zero` `one_smul` `zero_zpow` `zero_smul`
`meromorphicNFOn_inv` 📖	mathematical	—	`MeromorphicNFOn` `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`	—	`meromorphicNFAt_inv`
`meromorphicNFOn_mul_iff_left_of_analyticOnNhd` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicNFOn` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`mul_comm` `smul_eq_mul` `meromorphicNFOn_mul_iff_right_of_analyticOnNhd`
`meromorphicNFOn_mul_iff_right_of_analyticOnNhd` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicNFOn` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`smul_eq_mul` `meromorphicNFOn_smul_iff_right_of_analyticOnNhd`
`meromorphicNFOn_smul_iff_right_of_analyticOnNhd` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`MeromorphicNFOn` `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`	—	`meromorphicNFAt_smul_iff_right_of_analyticAt` `MeromorphicNFAt.smul_analytic`
`meromorphicNFOn_toMeromorphicNFOn` 📖	mathematical	—	`MeromorphicNFOn` `toMeromorphicNFOn`	—	`meromorphicNFAt_congr` `toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds` `meromorphicNFAt_toMeromorphicNFAt` `toMeromorphicNFOn_of_not_meromorphicOn` `AnalyticOnNhd.meromorphicNFOn` `analyticOnNhd_const`
`meromorphicOrderAt_toMeromorphicNFOn` 📖	mathematical	`MeromorphicOn` `Set` `Set.instMembership`	`meromorphicOrderAt` `toMeromorphicNFOn`	—	`meromorphicOrderAt_congr` `MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE`
`toMeromorphicNFAt_eq_self` 📖	mathematical	—	`toMeromorphicNFAt` `MeromorphicNFAt`	—	`meromorphicNFAt_toMeromorphicNFAt` `MeromorphicNFAt.meromorphicAt` `Function.update.congr_simp` `meromorphicOrderAt_eq_top_iff` `Filter.EventuallyEq.filter_mono` `nhdsWithin_le_nhds` `Int.instIsOrderedAddMonoid` `Function.update_self` `Filter.EventuallyEq.eq_of_nhds` `meromorphicOrderAt_eq_int_iff` `eventually_nhdsWithin_of_eventually_nhds` `sub_self` `WithTop.coe_eq_zero` `zpow_zero` `one_smul` `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `AnalyticAt.continuousAt` `PerfectSpace.not_isolated` `instPerfectSpace` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `zero_zpow` `MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt`
`toMeromorphicNFAt_of_not_meromorphicAt` 📖	mathematical	`MeromorphicAt`	`toMeromorphicNFAt` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`toMeromorphicNFOn_eqOn_codiscrete` 📖	mathematical	`MeromorphicOn`	`Filter.EventuallyEq` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `toMeromorphicNFOn`	—	`mem_codiscreteWithin` `sdiff_self` `Filter.principal_empty` `Filter.mp_mem` `MeromorphicOn.analyticAt_mem_codiscreteWithin` `Filter.univ_mem'` `toMeromorphicNFAt_eq_self` `AnalyticAt.meromorphicNFAt`
`toMeromorphicNFOn_eq_self` 📖	mathematical	—	`toMeromorphicNFOn` `MeromorphicNFOn`	—	`meromorphicNFOn_toMeromorphicNFOn` `MeromorphicNFOn.meromorphicOn` `toMeromorphicNFAt_eq_self`
`toMeromorphicNFOn_eq_self_on_compl` 📖	mathematical	`MeromorphicOn`	`Set.EqOn` `toMeromorphicNFOn` `Compl.compl` `Set` `Set.instCompl`	—	—
`toMeromorphicNFOn_eq_toMeromorphicNFAt` 📖	mathematical	`MeromorphicOn` `Set` `Set.instMembership`	`toMeromorphicNFOn` `toMeromorphicNFAt`	—	`Filter.EventuallyEq.eq_of_nhds` `Filter.EventuallyEq.trans` `toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds`
`toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds` 📖	mathematical	`MeromorphicOn` `Set` `Set.instMembership`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `toMeromorphicNFOn` `toMeromorphicNFAt`	—	`eventuallyEq_nhds_of_eventuallyEq_nhdsNE` `Filter.EventuallyEq.trans` `MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE` `MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt`
`toMeromorphicNFOn_of_not_meromorphicOn` 📖	mathematical	`MeromorphicOn`	`toMeromorphicNFOn` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—

---

← Back to Index