ZMod

📁 Source: Mathlib/NumberTheory/LSeries/ZMod.lean

Statistics

Metric	Count
Definitions `LFunction`, `completedLFunction`, `completedLFunction₀`	3
Theorems `LFunction_apply_zero_of_even`, `LFunction_def_even`, `LFunction_def_odd`, `LFunction_dft`, `LFunction_eq_LSeries`, `LFunction_eq_completed_div_gammaFactor_even`, `LFunction_eq_completed_div_gammaFactor_odd`, `LFunction_modOne_eq`, `LFunction_neg_two_mul_nat_add_one`, `LFunction_neg_two_mul_nat_sub_one`, `LFunction_one_sub`, `LFunction_residue_one`, `LFunction_stdAddChar_eq_expZeta`, `LSeriesSummable_of_one_lt_re`, `completedLFunction_const_mul`, `completedLFunction_def_even`, `completedLFunction_def_odd`, `completedLFunction_eq`, `completedLFunction_modOne_eq`, `completedLFunction_one_sub_even`, `completedLFunction_one_sub_odd`, `completedLFunction_zero`, `differentiableAt_LFunction`, `differentiableAt_completedLFunction`, `differentiable_LFunction_of_sum_zero`, `differentiable_completedLFunction`, `differentiable_completedLFunction₀`	27
Total	30

ZMod

Definitions

Name	Category	Theorems
`LFunction` 📖	CompOp	15 math math: `differentiableAt_LFunction`, `LFunction_modOne_eq`, `LFunction_stdAddChar_eq_expZeta`, `LFunction_one_sub`, `LFunction_eq_LSeries`, `LFunction_def_odd`, `LFunction_eq_completed_div_gammaFactor_even`, `LFunction_neg_two_mul_nat_sub_one`, `LFunction_eq_completed_div_gammaFactor_odd`, `LFunction_def_even`, `LFunction_neg_two_mul_nat_add_one`, `LFunction_apply_zero_of_even`, `LFunction_residue_one`, `differentiable_LFunction_of_sum_zero`, `LFunction_dft`
`completedLFunction` 📖	CompOp	12 math math: `completedLFunction_zero`, `completedLFunction_def_even`, `differentiableAt_completedLFunction`, `LFunction_eq_completed_div_gammaFactor_even`, `completedLFunction_def_odd`, `differentiable_completedLFunction`, `LFunction_eq_completed_div_gammaFactor_odd`, `completedLFunction_eq`, `completedLFunction_const_mul`, `completedLFunction_one_sub_odd`, `completedLFunction_one_sub_even`, `completedLFunction_modOne_eq`
`completedLFunction₀` 📖	CompOp	2 math math: `completedLFunction_eq`, `differentiable_completedLFunction₀`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LFunction_apply_zero_of_even` 📖	mathematical	`Function.Even` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing`	`LFunction` `Complex.instZero` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `AddSubgroup.normal_of_comm` `LFunction_def_even` `neg_zero` `Complex.cpow_zero` `Finset.sum_congr` `HurwitzZeta.hurwitzZetaEven_apply_zero` `mul_ite` `mul_div` `mul_neg_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `one_mul`
`LFunction_def_even` 📖	mathematical	`Function.Even` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing`	`LFunction` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `HurwitzZeta.hurwitzZetaEven` `DFunLike.coe` `AddMonoidHom` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`AddSubgroup.normal_of_comm` `Finset.sum_congr` `mul_add` `Distrib.leftDistribClass` `Finset.sum_add_distrib` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Complex.instIsAddTorsionFree` `Fintype.sum_equiv` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `HurwitzZeta.hurwitzZetaOdd_neg` `mul_neg`
`LFunction_def_odd` 📖	mathematical	`Function.Odd` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `Complex.instNeg`	`LFunction` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `HurwitzZeta.hurwitzZetaOdd` `DFunLike.coe` `AddMonoidHom` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`AddSubgroup.normal_of_comm` `Finset.sum_congr` `mul_add` `Distrib.leftDistribClass` `Finset.sum_add_distrib` `AddRightCancelSemigroup.toIsRightCancelAdd` `Complex.instIsAddTorsionFree` `Fintype.sum_equiv` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `HurwitzZeta.hurwitzZetaEven_neg` `neg_mul`
`LFunction_dft` 📖	mathematical	`ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Complex` `Complex.instZero`	`LFunction` `DFunLike.coe` `LinearEquiv` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Complex.addCommGroup` `Pi.Function.module` `Complex.instModuleSelf` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dft` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `Complex.instMul` `HurwitzZeta.expZeta` `AddMonoidHom` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`AddSubgroup.normal_of_comm` `LFunction_stdAddChar_eq_expZeta` `MulZeroClass.zero_mul` `RingHomInvPair.ids` `Finset.mul_sum` `Finset.sum_congr` `dft_def` `Finset.sum_comm` `Finset.sum_mul` `mul_assoc` `mul_comm` `neg_mul`
`LFunction_eq_LSeries` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`LFunction` `LSeries` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing`	—	`LFunction.eq_1` `LSeries.eq_1` `Finset.mul_sum` `Nat.sumByResidueClasses` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.instCompleteSpace` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `LSeriesSummable_of_one_lt_re` `Set.mem_Icc` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `div_le_one` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Nat.cast_le` `RCLike.charZero_rclike` `LT.lt.le` `val_lt` `AddSubgroup.normal_of_comm` `toAddCircle_apply` `HasSum.tsum_eq` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re` `mul_assoc` `tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `mul_comm` `Complex.cpow_neg` `Complex.ofReal_div` `add_comm` `add_div` `Complex.ofReal_add` `Complex.ofReal_mul` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `Nat.cast_ne_zero` `Complex.instCharZero` `one_div_mul_one_div` `mul_one_div` `Complex.mul_cpow_ofReal_nonneg` `add_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `mul_div_assoc` `Nat.cast_add` `natCast_zmod_val` `Nat.cast_mul` `natCast_self` `MulZeroClass.zero_mul` `add_zero` `LSeries.term_of_ne_zero'` `Complex.ne_zero_of_one_lt_re`
`LFunction_eq_completed_div_gammaFactor_even` 📖	mathematical	`Function.Even` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Complex.instZero`	`LFunction` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `completedLFunction` `Complex.Gammaℝ`	—	`AddSubgroup.normal_of_comm` `LFunction_def_even` `completedLFunction_def_even` `mul_div_assoc` `Finset.sum_div` `Finset.sum_congr` `ne_or_eq` `HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne` `toAddCircle_eq_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `MulZeroClass.zero_mul`
`LFunction_eq_completed_div_gammaFactor_odd` 📖	mathematical	`Function.Odd` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `Complex.instNeg`	`LFunction` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `completedLFunction` `Complex.Gammaℝ` `Complex.instAdd` `Complex.instOne`	—	`AddSubgroup.normal_of_comm` `LFunction_def_odd` `Finset.sum_congr` `completedLFunction_def_odd` `mul_div_assoc` `Finset.sum_div`
`LFunction_modOne_eq` 📖	mathematical	—	`LFunction` `Complex` `Complex.instMul` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `riemannZeta`	—	`Nat.cast_one` `Complex.one_cpow` `Finset.sum_congr` `Finset.singleton_eq_univ` `Unique.instSubsingleton` `Finset.sum_singleton` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `HurwitzZeta.hurwitzZeta_zero` `one_mul`
`LFunction_neg_two_mul_nat_add_one` 📖	mathematical	`Function.Even` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing`	`LFunction` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.instAdd` `Complex.instOne` `Complex.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `AddSubgroup.normal_of_comm` `LFunction.congr_simp` `LFunction_def_even` `Finset.sum_congr` `HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one` `MulZeroClass.mul_zero` `Finset.sum_const_zero`
`LFunction_neg_two_mul_nat_sub_one` 📖	mathematical	`Function.Odd` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `Complex.instNeg`	`LFunction` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.instOne` `Complex.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `AddSubgroup.normal_of_comm` `LFunction.congr_simp` `LFunction_def_odd` `Finset.sum_congr` `HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat_sub_one` `MulZeroClass.mul_zero` `Finset.sum_const_zero`
`LFunction_one_sub` 📖	mathematical	`ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Complex` `Complex.instZero`	`LFunction` `Complex.instSub` `Complex.instOne` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.instNeg` `Complex.Gamma` `Complex.instAdd` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.I` `DFunLike.coe` `LinearEquiv` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Complex.addCommGroup` `Pi.Function.module` `Complex.instModuleSelf` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dft` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `LFunction.eq_1` `AddSubgroup.normal_of_comm` `eq_or_ne` `MulZeroClass.zero_mul` `HurwitzZeta.hurwitzZeta_one_sub` `Iff.not` `toAddCircle_eq_zero` `Finset.sum_congr` `mul_assoc` `mul_comm` `neg_sub` `LFunction_dft` `neg_zero` `Equiv.Perm.sum_comp` `Finset.coe_univ` `Equiv.neg_apply` `neg_neg` `Finset.mul_sum` `Distrib.leftDistribClass` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `add_comm`
`LFunction_residue_one` 📖	mathematical	—	`Filter.Tendsto` `Complex` `Complex.instMul` `Complex.instSub` `Complex.instOne` `LFunction` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds` `Finset.sum` `ZMod` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNatCast`	—	`Finset.mul_sum` `tendsto_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `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` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `one_div` `Complex.cpow_neg_one` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `tendsto_const_nhds` `Filter.Tendsto.mono_left` `Continuous.tendsto` `Continuous.const_cpow` `ContinuousNeg.continuous_neg` `IsTopologicalRing.toContinuousNeg` `NeZero.charZero` `nhdsWithin_le_nhds` `HurwitzZeta.hurwitzZeta_residue_one`
`LFunction_stdAddChar_eq_expZeta` 📖	mathematical	—	`LFunction` `DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `AddChar.instFunLike` `stdAddChar` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HurwitzZeta.expZeta` `AddMonoidHom` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`isOpen_compl_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `AddSubgroup.normal_of_comm` `DifferentiableOn.analyticOnNhd` `Complex.instCompleteSpace` `DifferentiableAt.differentiableWithinAt` `differentiableAt_LFunction` `Finset.sum_congr` `mul_comm` `AddChar.sum_mulShift` `instIsDomain` `isPrimitive_stdAddChar` `CharP.cast_eq_zero` `CharP.ofCharZero` `Complex.instCharZero` `HurwitzZeta.differentiableAt_expZeta` `toAddCircle_eq_zero` `IsConnected.isPreconnected` `isConnected_compl_singleton_of_one_lt_rank` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `Complex.rank_real_complex` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `PreconnectedSpace.isPreconnected_univ` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `ContractibleSpace.instPathConnectedSpace` `RealTopologicalVectorSpace.contractibleSpace` `IsOpen.mem_nhds` `Continuous.isOpen_preimage` `Complex.continuous_re` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq` `Filter.mp_mem` `Filter.univ_mem'`
`LSeriesSummable_of_one_lt_re` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`LSeriesSummable` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing`	—	`Finset.Nonempty.image` `Finset.univ_nonempty` `LSeriesSummable_of_bounded_of_one_lt_re` `Finset.le_max'` `Finset.mem_image_of_mem` `Finset.mem_univ`
`completedLFunction_const_mul` 📖	mathematical	—	`completedLFunction` `Complex` `Complex.instMul`	—	`Finset.sum_congr` `Finset.mul_sum` `mul_add` `Distrib.leftDistribClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`completedLFunction_def_even` 📖	mathematical	`Function.Even` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing`	`completedLFunction` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `HurwitzZeta.completedHurwitzZetaEven` `DFunLike.coe` `AddMonoidHom` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`AddSubgroup.normal_of_comm` `Function.Odd.sum_eq_zero` `Complex.instIsAddTorsionFree` `Function.Even.mul_odd` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `HurwitzZeta.completedHurwitzZetaOdd_neg` `completedLFunction.eq_1` `MulZeroClass.mul_zero` `add_zero`
`completedLFunction_def_odd` 📖	mathematical	`Function.Odd` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `Complex.instNeg`	`completedLFunction` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `HurwitzZeta.completedHurwitzZetaOdd` `DFunLike.coe` `AddMonoidHom` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`AddSubgroup.normal_of_comm` `Function.Odd.sum_eq_zero` `Complex.instIsAddTorsionFree` `Function.Odd.mul_even` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `HurwitzZeta.completedHurwitzZetaEven_neg` `completedLFunction.eq_1` `MulZeroClass.mul_zero` `zero_add`
`completedLFunction_eq` 📖	mathematical	—	`completedLFunction` `Complex` `Complex.instSub` `completedLFunction₀` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `Complex.instOne`	—	`Finset.sum_congr` `HurwitzZeta.completedHurwitzZetaEven_eq` `div_eq_mul_inv` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `mul_sub` `mul_ite` `MulZeroClass.mul_zero` `Finset.sum_sub_distrib` `Fintype.sum_ite_eq'` `mul_assoc` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`
`completedLFunction_modOne_eq` 📖	mathematical	—	`completedLFunction` `Complex` `Complex.instMul` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `completedRiemannZeta`	—	`AddSubgroup.normal_of_comm` `completedLFunction_def_even` `Unique.instSubsingleton` `Nat.cast_one` `Complex.one_cpow` `one_mul` `Finset.singleton_eq_univ` `Finset.sum_singleton` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `HurwitzZeta.completedHurwitzZetaEven_zero`
`completedLFunction_one_sub_even` 📖	mathematical	`Function.Even` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `Complex.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`completedLFunction` `Complex.instSub` `Complex.instOne` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `DFunLike.coe` `LinearEquiv` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Complex.addCommGroup` `Pi.Function.module` `Complex.instModuleSelf` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dft`	—	`RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `two_ne_zero` `CharZero.NeZero.two` `Complex.instCharZero` `OfNat.ofNat_ne_one` `IsOpen.inter` `IsOpen.union` `isOpen_compl_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `isOpen_const` `Set.Countable.union` `Set.ext` `Set.union_self` `Set.compl_empty` `Set.union_empty` `Set.union_singleton` `Set.instLawfulSingleton` `IsConnected.isPreconnected` `Set.Countable.isConnected_compl_of_one_lt_rank` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Complex.rank_real_complex` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `DifferentiableOn.analyticOnNhd` `Complex.instCompleteSpace` `DifferentiableAt.differentiableWithinAt` `DifferentiableAt.comp` `differentiableAt_completedLFunction` `sub_ne_zero` `Iff.not` `sub_eq_self` `DifferentiableAt.const_sub` `differentiableAt_id` `DifferentiableAt.mul` `DifferentiableAt.const_cpow` `DifferentiableAt.sub_const` `NeZero.charZero` `dft_apply_zero` `dft_dft` `neg_zero` `smul_zero` `IsOpen.mem_nhds` `Continuous.isOpen_preimage` `Complex.continuous_re` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Filter.eventually_of_mem` `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`
`completedLFunction_one_sub_odd` 📖	mathematical	`Function.Odd` `ZMod` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `commRing` `Complex.instNeg`	`completedLFunction` `Complex.instSub` `Complex.instOne` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Complex.I` `DFunLike.coe` `LinearEquiv` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Complex.addCommGroup` `Pi.Function.module` `Complex.instModuleSelf` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dft`	—	`RingHomInvPair.ids` `Differentiable.comp` `differentiable_completedLFunction` `Function.Odd.map_zero` `Complex.instIsAddTorsionFree` `Function.Odd.sum_eq_zero` `Differentiable.const_sub` `differentiable_id` `Differentiable.mul` `Differentiable.mul_const` `Differentiable.const_cpow` `Differentiable.sub_const` `NeZero.charZero` `Complex.instCharZero` `dft_odd_iff` `Nat.instAtLeastTwoHAddOfNat` `IsOpen.mem_nhds` `Continuous.isOpen_preimage` `Complex.continuous_re` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Filter.mp_mem` `Filter.univ_mem'` `AnalyticOnNhd.eq_of_eventuallyEq` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `ContractibleSpace.instPathConnectedSpace` `RealTopologicalVectorSpace.contractibleSpace` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Complex.analyticOnNhd_univ_iff_differentiable` `Complex.instCompleteSpace`
`completedLFunction_zero` 📖	mathematical	—	`completedLFunction` `Pi.instZero` `ZMod` `Complex` `Complex.instZero`	—	`Finset.sum_congr` `MulZeroClass.zero_mul` `Finset.sum_const_zero` `MulZeroClass.mul_zero` `zero_add`
`differentiableAt_LFunction` 📖	mathematical	`Finset.sum` `ZMod` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `Complex.instZero`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `LFunction`	—	`DifferentiableAt.mul` `DifferentiableAt.fun_comp'` `differentiableAt_const_cpow_of_neZero` `NeZero.charZero` `Complex.instCharZero` `DifferentiableAt.fun_neg` `differentiableAt_id` `ne_or_eq` `DifferentiableAt.fun_sum` `DifferentiableAt.const_mul` `HurwitzZeta.differentiableAt_hurwitzZeta` `AddSubgroup.normal_of_comm` `HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div` `Finset.sum_congr` `mul_sub` `Finset.sum_sub_distrib` `MulZeroClass.zero_mul` `sub_zero`
`differentiableAt_completedLFunction` 📖	mathematical	`ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Complex` `Complex.instZero` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `completedLFunction`	—	`completedLFunction_eq` `mul_div_assoc` `DifferentiableAt.sub` `differentiable_completedLFunction₀` `DifferentiableAt.mul` `DifferentiableAt.fun_comp'` `differentiableAt_const_cpow_of_neZero` `NeZero.charZero` `Complex.instCharZero` `DifferentiableAt.fun_neg` `differentiableAt_id` `DifferentiableAt.div` `differentiableAt_const` `zero_div` `DifferentiableAt.const_sub` `sub_ne_zero`
`differentiable_LFunction_of_sum_zero` 📖	mathematical	`Finset.sum` `ZMod` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype` `Complex.instZero`	`Differentiable` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `LFunction`	—	`differentiableAt_LFunction`
`differentiable_completedLFunction` 📖	mathematical	`ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Complex` `Complex.instZero` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `fintype`	`Differentiable` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `completedLFunction`	—	`differentiableAt_completedLFunction`
`differentiable_completedLFunction₀` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `completedLFunction₀`	—	`Differentiable.add` `Differentiable.mul` `Differentiable.fun_comp` `differentiable_const_cpow_of_neZero` `NeZero.charZero` `Complex.instCharZero` `Differentiable.fun_neg` `differentiable_id` `Differentiable.fun_sum` `Differentiable.const_mul` `HurwitzZeta.differentiable_completedHurwitzZetaEven₀` `HurwitzZeta.differentiable_completedHurwitzZetaOdd`

---

← Back to Index