Order

📁 Source: Mathlib/Analysis/Analytic/Order.lean

Statistics

Metric	Count
Definitions `analyticOrderAt`, `analyticOrderNatAt`	2
Theorems `analyticOrderAt_comp`, `analyticOrderAt_deriv_add_one`, `analyticOrderAt_eq_natCast`, `analyticOrderAt_eq_zero`, `analyticOrderAt_ne_top`, `analyticOrderAt_ne_zero`, `analyticOrderAt_sub_eq_one_of_deriv_ne_zero`, `analyticOrderNatAt_eq_iff`, `exists_eq_sum_add_pow_mul`, `exists_eventuallyEq_sum_add_pow_mul`, `analyticOrderAt_ne_top_of_isPreconnected`, `codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top`, `codiscrete_setOf_analyticOrderAt_eq_zero_or_top`, `exists_analyticOrderAt_ne_top_iff_forall`, `isClopen_setOf_analyticOrderAt_eq_top`, `preimage_zero_mem_codiscrete`, `preimage_zero_mem_codiscreteWithin`, `cast_analyticOrderNatAt`, `analyticOrderAt_add_eq_left_of_lt`, `analyticOrderAt_add_eq_right_of_lt`, `analyticOrderAt_add_of_ne`, `analyticOrderAt_centeredMonomial`, `analyticOrderAt_comp_of_deriv_ne_zero`, `analyticOrderAt_congr`, `analyticOrderAt_eq_top`, `analyticOrderAt_eq_zero`, `analyticOrderAt_id`, `analyticOrderAt_mul`, `analyticOrderAt_mul_eq_top_of_left`, `analyticOrderAt_mul_eq_top_of_right`, `analyticOrderAt_ne_zero`, `analyticOrderAt_neg`, `analyticOrderAt_of_not_analyticAt`, `analyticOrderAt_pow`, `analyticOrderAt_smul`, `analyticOrderAt_smul_eq_top_of_left`, `analyticOrderAt_smul_eq_top_of_right`, `analyticOrderNatAt_mul`, `analyticOrderNatAt_of_not_analyticAt`, `analyticOrderNatAt_pow`, `apply_eq_zero_of_analyticOrderAt_ne_zero`, `apply_eq_zero_of_analyticOrderNatAt_ne_zero`, `eventuallyConst_iff_analyticOrderAt_sub_eq_top`, `le_analyticOrderAt_add`, `le_analyticOrderAt_sub`, `natCast_le_analyticOrderAt`, `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero`	47
Total	49

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOrderAt_comp` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Filter.EventuallyConst.comp` `eventuallyConst_iff_analyticOrderAt_sub_eq_top` `ENat.mul_top` `sub_zero` `MulZeroClass.zero_mul` `analyticOrderAt_eq_top` `Filter.EventuallyEq.comp_tendsto` `continuousAt` `ENat.top_mul` `analyticOrderAt_ne_zero` `fun_sub` `analyticAt_const` `sub_eq_zero` `ENat.ne_top_iff_exists` `ENat.coe_mul` `analyticOrderAt_eq_natCast` `comp` `fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `fun_pow` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Filter.mp_mem` `Filter.univ_mem'` `mul_pow` `SemigroupAction.mul_smul` `mul_comm` `pow_mul`
`analyticOrderAt_deriv_add_one` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `analyticOrderAt` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`eventually_nhds_iff` `Filter.mp_mem` `IsOpen.mem_nhds` `Filter.univ_mem'` `Filter.EventuallyEq.deriv_eq` `Filter.eventuallyEq_of_mem` `deriv_const'` `top_add` `analyticOrderAt_eq_zero` `fun_sub` `analyticAt_const` `ENat.coe_zero` `Nat.cast_succ` `analyticOrderAt_eq_natCast` `Filter.Eventually.and` `eventually_analyticAt` `Filter.eventually_of_mem` `deriv_add_const` `deriv_fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `DifferentiableAt.fun_pow` `DifferentiableAt.sub_const` `differentiableAt_id` `differentiableAt` `deriv_fun_pow` `Nat.cast_add` `Nat.cast_one` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `deriv_fun_sub` `deriv_id''` `sub_zero` `mul_one` `SemigroupAction.mul_smul` `add_smul` `Nat.cast_smul_eq_nsmul` `one_smul` `analyticOrderAt_congr` `fun_const_smul` `smulCommClass_self` `fun_smul` `fun_pow` `analyticAt_id` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `Nat.cast_zero` `Filter.Eventually.of_forall` `SMulCommClass.smul_comm` `AddMonoid.nat_smulCommClass` `Pi.add_def` `analyticOrderAt_add_eq_right_of_lt` `Order.succ_le_iff_of_not_isMax` `not_isMax_iff` `ENat.coe_lt_top` `ENat.succ_def` `Nat.cast_add_one` `natCast_le_analyticOrderAt` `deriv`
`analyticOrderAt_eq_natCast` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `ENat` `ENat.instNatCast` `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` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `nhds` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `exists_eventuallyEq_pow_smul_nonzero_iff` `unique_eventuallyEq_pow_smul_nonzero`
`analyticOrderAt_eq_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `ENat` `instZeroENat`	—	—
`analyticOrderAt_ne_top` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `analyticOrderNatAt`	—	`analyticOrderAt_eq_natCast`
`analyticOrderAt_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Iff.not_left` `analyticOrderAt_eq_zero`
`analyticOrderAt_sub_eq_one_of_deriv_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Filter.EventuallyEq.deriv_eq` `deriv_const` `Nat.cast_one` `analyticOrderAt_eq_natCast` `fun_sub` `analyticAt_const` `eq_of_ge_of_le` `Filter.Eventually.self_of_nhds` `sub_self` `pow_zero` `one_smul` `Mathlib.Tactic.Contrapose.contrapose₂` `deriv_add_const` `deriv_fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `DifferentiableAt.fun_pow` `DifferentiableAt.sub_const` `differentiableAt_id` `differentiableAt` `deriv_fun_pow` `zero_pow` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `zero_smul` `add_zero`
`analyticOrderNatAt_eq_iff` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderNatAt` `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` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `nhds` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`Nat.cast_analyticOrderNatAt` `analyticOrderAt_eq_natCast`
`exists_eq_sum_add_pow_mul` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.sum` `Finset.range` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `NormedSpace.toModule` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Monoid.toNatPow` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Nat.factorial` `iteratedDeriv`	—	`exists_eventuallyEq_sum_add_pow_mul` `Filter.eventually_iff_exists_mem` `congr` `Filter.mp_mem` `Filter.univ_mem'` `smul_inv_smul₀` `Mathlib.Tactic.Contrapose.contrapose₄` `mem_of_mem_nhds` `pow_eq_zero_iff'` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Module.NF.eq_const_cons` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add`
`exists_eventuallyEq_sum_add_pow_mul` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	`Filter.Eventually` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.sum` `Finset.range` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `NormedSpace.toModule` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Monoid.toNatPow` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Nat.factorial` `iteratedDeriv` `nhds` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`Finset.analyticAt_fun_sum` `fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `div_const` `fun_pow` `analyticAt_id` `analyticAt_const` `sub_zero` `natCast_le_analyticOrderAt` `fun_sub` `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` `iteratedDeriv_fun_sub` `contDiffAt` `iteratedDeriv_fun_sum` `ContDiffAt.smul_const` `ContDiffAt.div_const` `ContDiffAt.pow` `contDiffAt_fun_id` `Finset.sum_congr` `iteratedDeriv_smul_const` `iteratedDeriv_div_const` `iteratedDeriv_fun_pow_zero` `Nat.cast_ite` `CharP.cast_eq_zero` `CharP.ofCharZero` `ite_div` `div_self` `zero_div` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq_of_mem` `Finset.mem_range` `sub_self`

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOrderAt_ne_top_of_isPreconnected` 📖	—	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `IsPreconnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Set` `Set.instMembership`	—	—	`exists_analyticOrderAt_ne_top_iff_forall` `Set.nonempty_of_mem`
`codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Set` `Filter` `Filter.instMembership` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `setOf` `ENat` `analyticOrderAt` `instZeroENat` `Top.top` `instTopENat`	—	`AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` `Filter.mp_mem` `eventually_nhdsWithin_of_eventually_nhds` `Filter.Eventually.eventually_nhds` `Filter.univ_mem'` `AnalyticAt.analyticOrderAt_eq_zero`
`codiscrete_setOf_analyticOrderAt_eq_zero_or_top` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Set` `Set.Elem` `Filter` `Filter.instMembership` `Filter.codiscrete` `instTopologicalSpaceSubtype` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `setOf` `ENat` `analyticOrderAt` `instZeroENat` `Top.top` `instTopENat`	—	`AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` `Filter.mp_mem` `eventually_nhdsWithin_of_eventually_nhds` `Filter.Eventually.eventually_nhds` `Filter.univ_mem'` `AnalyticAt.analyticOrderAt_eq_zero`
`exists_analyticOrderAt_ne_top_iff_forall` 📖	—	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	—	`Subtype.connectedSpace` `ConnectedSpace.toNonempty` `isClopen_iff` `ConnectedSpace.toPreconnectedSpace` `isClopen_setOf_analyticOrderAt_eq_top`
`isClopen_setOf_analyticOrderAt_eq_top` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`IsClopen` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `setOf` `ENat` `analyticOrderAt` `Top.top` `instTopENat`	—	`isOpen_compl_iff` `isOpen_iff_forall_mem_open` `AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` `analyticOrderAt_eq_top` `eventually_nhds_iff` `eventually_nhdsWithin_iff` `AnalyticAt.analyticOrderAt_eq_zero` `Subtype.coe_ne_coe` `ENat.zero_ne_top` `isOpen_induced`
`preimage_zero_mem_codiscrete` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Set.univ`	`Set` `Filter` `Filter.instMembership` `Filter.codiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Set.preimage` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`preimage_zero_mem_codiscreteWithin` `isConnected_univ`
`preimage_zero_mem_codiscreteWithin` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Set` `Set.instMembership` `IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Filter` `Filter.instMembership` `Filter.codiscreteWithin` `Set.preimage` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Filter.mp_mem` `Filter.self_mem_codiscreteWithin` `codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top` `Filter.univ_mem'` `exists_analyticOrderAt_ne_top_iff_forall` `AnalyticAt.analyticOrderAt_eq_zero`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_analyticOrderNatAt` 📖	mathematical	—	`ENat` `ENat.instNatCast` `analyticOrderNatAt` `analyticOrderAt`	—	`ENat.coe_toNat`

(root)

Definitions

Name	Category	Theorems
`analyticOrderAt` 📖	CompOp	28 math math: `AnalyticAt.meromorphicOrderAt_eq`, `analyticOrderAt_eq_top`, `Nat.cast_analyticOrderNatAt`, `analyticOrderAt_comp_of_deriv_ne_zero`, `analyticOrderAt_centeredMonomial`, `natCast_le_analyticOrderAt`, `AnalyticAt.analyticOrderAt_deriv_add_one`, `analyticOrderAt_congr`, `analyticOrderAt_mul`, `AnalyticAt.analyticOrderAt_eq_natCast`, `analyticOrderAt_neg`, `AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top`, `le_analyticOrderAt_sub`, `le_analyticOrderAt_add`, `analyticOrderAt_pow`, `analyticOrderAt_id`, `AnalyticAt.analyticOrderAt_comp`, `AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top`, `AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top`, `eventuallyConst_iff_analyticOrderAt_sub_eq_top`, `analyticOrderAt_of_not_analyticAt`, `analyticOrderAt_smul`, `analyticOrderAt_eq_zero`, `AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero`, `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero`, `analyticOrderAt_add_of_ne`, `MeromorphicAt.meromorphicOrderAt_comp`, `AnalyticAt.analyticOrderAt_eq_zero`
`analyticOrderNatAt` 📖	CompOp	6 math math: `Nat.cast_analyticOrderNatAt`, `AnalyticAt.analyticOrderNatAt_eq_iff`, `analyticOrderNatAt_of_not_analyticAt`, `AnalyticAt.analyticOrderAt_ne_top`, `analyticOrderNatAt_pow`, `analyticOrderNatAt_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOrderAt_add_eq_left_of_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `analyticOrderAt`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`le_antisymm` `add_sub_cancel_right` `LT.lt.not_ge` `le_analyticOrderAt_sub` `inf_of_le_left` `LT.lt.le` `le_analyticOrderAt_add`
`analyticOrderAt_add_eq_right_of_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `analyticOrderAt`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add_comm` `analyticOrderAt_add_eq_left_of_lt`
`analyticOrderAt_add_of_ne` 📖	mathematical	—	`analyticOrderAt` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`Ne.lt_or_gt` `inf_of_le_left` `LT.lt.le` `analyticOrderAt_add_eq_left_of_lt` `inf_of_le_right` `analyticOrderAt_add_eq_right_of_lt`
`analyticOrderAt_centeredMonomial` 📖	mathematical	—	`analyticOrderAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ENat` `ENat.instNatCast`	—	`AnalyticAt.analyticOrderAt_eq_natCast` `AnalyticAt.pow` `AnalyticAt.fun_sub` `analyticAt_id` `analyticAt_const` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mul_one`
`analyticOrderAt_comp_of_deriv_ne_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt`	—	`AnalyticAt.analyticOrderAt_comp` `AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero` `mul_one` `analyticOrderAt_of_not_analyticAt` `analyticAt_comp_iff_of_deriv_ne_zero`
`analyticOrderAt_congr` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField`	`analyticOrderAt`	—	`ENat.eq_of_forall_natCast_le_iff` `AnalyticAt.congr` `Filter.EventuallyEq.congr_left` `analyticOrderAt_of_not_analyticAt` `Filter.EventuallyEq.symm`
`analyticOrderAt_eq_top` 📖	mathematical	—	`analyticOrderAt` `Top.top` `ENat` `instTopENat` `Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField`	—	`analyticAt_congr`
`analyticOrderAt_eq_zero` 📖	mathematical	—	`analyticOrderAt` `ENat` `instZeroENat` `AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	—	`ENat.coe_zero` `AnalyticAt.analyticOrderAt_eq_natCast` `Filter.Eventually.self_of_nhds` `sub_self` `pow_zero` `one_smul` `analyticOrderAt_of_not_analyticAt`
`analyticOrderAt_id` 📖	mathematical	—	`analyticOrderAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`AnalyticAt.analyticOrderAt_eq_natCast` `analyticAt_id` `analyticAt_const` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_zero` `pow_one` `mul_one`
`analyticOrderAt_mul` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ENat` `Distrib.toAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`analyticOrderAt_smul`
`analyticOrderAt_mul_eq_top_of_left` 📖	mathematical	`analyticOrderAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Top.top` `ENat` `instTopENat`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`analyticOrderAt_smul_eq_top_of_left`
`analyticOrderAt_mul_eq_top_of_right` 📖	mathematical	`analyticOrderAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Top.top` `ENat` `instTopENat`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`analyticOrderAt_smul_eq_top_of_right`
`analyticOrderAt_ne_zero` 📖	mathematical	—	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`analyticOrderAt_neg` 📖	mathematical	—	`analyticOrderAt` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ENat.eq_of_forall_natCast_le_iff` `AnalyticAt.neg` `Equiv.exists_congr` `smul_neg` `analyticOrderAt_of_not_analyticAt` `Iff.not` `analyticAt_neg`
`analyticOrderAt_of_not_analyticAt` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `ENat` `instZeroENat`	—	—
`analyticOrderAt_pow` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `Monoid.toNatPow` `Pi.monoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ENat` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`pow_zero` `zero_nsmul` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `pow_add` `pow_one` `analyticOrderAt_mul` `AnalyticAt.pow` `nsmul_eq_mul` `Nat.cast_add` `Nat.cast_one` `add_mul` `Distrib.rightDistribClass` `one_mul`
`analyticOrderAt_smul` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderAt` `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` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`analyticOrderAt_smul_eq_top_of_left` `top_add` `analyticOrderAt_smul_eq_top_of_right` `add_top` `AnalyticAt.analyticOrderAt_ne_top` `Nat.cast_analyticOrderNatAt` `ENat.coe_add` `AnalyticAt.analyticOrderAt_eq_natCast` `AnalyticAt.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `eventually_nhds_iff` `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.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` `Mathlib.Tactic.Ring.add_congr` `IsOpen.inter`
`analyticOrderAt_smul_eq_top_of_left` 📖	mathematical	`analyticOrderAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Top.top` `ENat` `instTopENat`	`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`	—	`analyticOrderAt_eq_top` `eventually_nhds_iff` `zero_smul`
`analyticOrderAt_smul_eq_top_of_right` 📖	mathematical	`analyticOrderAt` `Top.top` `ENat` `instTopENat`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`analyticOrderAt_eq_top` `eventually_nhds_iff` `smul_zero`
`analyticOrderNatAt_mul` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderNatAt` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`analyticOrderAt_mul` `ENat.toNat_add`
`analyticOrderNatAt_of_not_analyticAt` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderNatAt`	—	`analyticOrderAt_of_not_analyticAt`
`analyticOrderNatAt_pow` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`analyticOrderNatAt` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `AddMonoid.toNatSMul` `Nat.instAddMonoid`	—	`analyticOrderAt_pow` `nsmul_eq_mul` `ENat.toNat_mul`
`apply_eq_zero_of_analyticOrderAt_ne_zero` 📖	mathematical	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`analyticOrderAt_of_not_analyticAt`
`apply_eq_zero_of_analyticOrderNatAt_ne_zero` 📖	mathematical	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`analyticOrderAt_of_not_analyticAt`
`eventuallyConst_iff_analyticOrderAt_sub_eq_top` 📖	mathematical	—	`Filter.EventuallyConst` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `analyticOrderAt` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Top.top` `ENat` `instTopENat`	—	`AddTorsor.nonempty` `Filter.Eventually.self_of_nhds`
`le_analyticOrderAt_add` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `analyticOrderAt` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`ENat.forall_natCast_le_iff_le` `AnalyticAt.add` `Filter.mp_mem` `Filter.univ_mem'` `smul_add` `analyticOrderAt_of_not_analyticAt` `inf_of_le_right` `inf_of_le_left`
`le_analyticOrderAt_sub` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `analyticOrderAt` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `analyticOrderAt_neg` `le_analyticOrderAt_add`
`natCast_le_analyticOrderAt` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `analyticOrderAt` `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` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `nhds` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`analyticAt_const` `smul_zero` `AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff` `ENat.coe_le_coe` `AnalyticAt.fun_smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `AnalyticAt.fun_pow` `AnalyticAt.fun_sub` `analyticAt_id` `Filter.mp_mem` `Filter.univ_mem'` `SemigroupAction.mul_smul` `pow_add` `Mathlib.Tactic.Contrapose.contrapose₂` `ContinuousAt.smul` `IsBoundedSMul.continuousSMul` `ContinuousAt.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousAt_id'` `continuousAt_const` `AnalyticAt.continuousAt` `tendsto_nhds_unique_of_eventuallyEq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `PerfectSpace.not_isolated` `instPerfectSpace` `ContinuousAt.continuousWithinAt` `Filter.Eventually.filter_mono` `nhdsWithin_le_nhds` `self_mem_nhdsWithin` `pow_sub₀` `sub_ne_zero_of_ne` `SMulCommClass.smul_comm` `smulCommClass_self` `inv_smul_eq_iff₀` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `sub_self` `zero_pow` `zero_smul`
`natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `analyticOrderAt` `iteratedDeriv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`CharP.cast_eq_zero` `CharP.ofCharZero` `Nat.instCanonicallyOrderedAdd` `instIsEmptyFalse` `sub_zero` `AnalyticAt.analyticOrderAt_deriv_add_one` `Nat.cast_add` `Nat.cast_one` `AnalyticAt.deriv` `iteratedDeriv_zero` `iteratedDeriv_succ'` `analyticOrderAt_eq_zero` `Unique.instSubsingleton` `NeZero.charZero_one` `Nat.instNoMaxOrder`

---

← Back to Index