GammaDeriv

📁 Source: Mathlib/NumberTheory/Harmonic/GammaDeriv.lean

Statistics

Metric	Count
Definitions	0
Theorems deriv_Gamma_nat, differentiableAt_Gamma_nat_add_one, hasDerivAt_Gamma_nat, hasDerivAt_Gamma_one, hasDerivAt_Gamma_one_half, hasDerivAt_Gammaℂ_one, hasDerivAt_Gammaℝ_one, deriv_Gamma_nat, eulerMascheroniConstant_eq_neg_deriv, hasDerivAt_Gamma_nat, hasDerivAt_Gamma_one, hasDerivAt_Gamma_one_half	12
Total	12

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_Gamma_nat 📖	mathematical	—	deriv Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instAdd instNatCast instOne instMul Nat.factorial instNeg ofReal Real.eulerMascheroniConstant instRatCast harmonic	—	HasDerivAt.deriv hasDerivAt_Gamma_nat
differentiableAt_Gamma_nat_add_one 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instAdd instNatCast instOne	—	differentiableAt_Gamma ne_of_gt add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
hasDerivAt_Gamma_nat 📖	mathematical	—	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Gamma instMul instNatCast Nat.factorial instNeg ofReal Real.eulerMascheroniConstant instRatCast harmonic instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasDerivAt.congr_simp Nat.cast_one Nat.cast_add ofReal_add differentiableAt_Gamma_nat_add_one Real.hasDerivAt_Gamma_nat Gamma_ofReal
hasDerivAt_Gamma_one 📖	mathematical	—	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Gamma instNeg ofReal Real.eulerMascheroniConstant instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasDerivAt.congr_simp Nat.cast_one Rat.cast_zero add_zero mul_neg one_mul Nat.cast_zero zero_add hasDerivAt_Gamma_nat
hasDerivAt_Gamma_one_half 📖	mathematical	—	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Gamma instMul instNeg ofReal Real.sqrt Real.pi Real.eulerMascheroniConstant instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log DivInvMonoid.toDiv instDivInvMonoid instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Nat.instAtLeastTwoHAddOfNat differentiableAt_Gamma ofReal_natCast ofReal_neg LT.lt.ne' LE.le.trans_lt neg_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg Real.instIsOrderedRing one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.hasDerivAt_Gamma_one_half Gamma_ofReal HasDerivAt.congr_simp neg_mul one_div ofReal_mul ofReal_add ofNat_log ofReal_inv
hasDerivAt_Gammaℂ_one 📖	mathematical	—	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Gammaℂ DivInvMonoid.toDiv instDivInvMonoid instNeg ofReal Real.eulerMascheroniConstant log instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi instOne	—	Nat.instAtLeastTwoHAddOfNat IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul HasDerivAt.const_cpow hasDerivAt_neg' Nat.cast_zero LT.lt.ne' Real.two_pi_pos HasDerivAt.congr_deriv HasDerivAt.const_mul mul_neg_one mul_neg cpow_neg_one div_eq_inv_mul mul_div_assoc mul_div_mul_left two_ne_zero CharZero.NeZero.two instCharZero neg_div IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.mul hasDerivAt_Gamma_one add_comm neg_add add_div mul_one_div mul_comm div_self div_div div_eq_mul_inv mul_one Gamma_one
hasDerivAt_Gammaℝ_one 📖	mathematical	—	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Gammaℝ DivInvMonoid.toDiv instDivInvMonoid instNeg ofReal Real.eulerMascheroniConstant log instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi instOne	—	Nat.instAtLeastTwoHAddOfNat Real.sqrt_eq_rpow ofReal_cpow LT.lt.le Real.pi_pos ofReal_div ofReal_one ofReal_ofNat ofReal_ne_zero ne_of_gt Real.sqrt_pos_of_pos IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul HasDerivAt.const_cpow HasDerivAt.div_const hasDerivAt_neg NeZero.charZero_one instCharZero HasDerivAt.congr_deriv mul_assoc mul_div_assoc mul_neg_one neg_div cpow_neg div_eq_inv_mul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.comp hasDerivAt_Gamma_one_half hasDerivAt_id mul_one_div HasDerivAt.mul Gamma_one_half_eq div_mul_cancel₀ mul_neg inv_mul_cancel₀ neg_one_mul add_div neg_add add_comm add_assoc ofReal_log zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ofReal_mul Nat.cast_ofNat Real.log_pow ofReal_add Real.log_mul pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' RCLike.charZero_rclike Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat le_of_lt mul_pos Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 neg_add_rev

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_Gamma_nat 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Gamma instAdd instNatCast instOne instMul Nat.factorial instNeg eulerMascheroniConstant instRatCast harmonic	—	convexOn_log_Gamma Gamma_add_one LT.lt.ne' log_mul Gamma_pos_of_pos add_comm DifferentiableAt.log differentiableAt_Gamma ne_of_gt lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.sub_neg_of_lt Gamma_ne_zero deriv_comp_add_const one_div deriv_log deriv_add differentiableAt_log Filter.EventuallyEq.deriv_eq Filter.mp_mem eventually_gt_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid Filter.univ_mem' CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_add Rat.cast_zero add_zero Nat.cast_succ Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.cast_nonneg' instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Nat.cast_one harmonic_succ Nat.cast_add Rat.cast_add Rat.cast_inv Rat.cast_natCast Rat.cast_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_congr LE.le.trans le_of_eq slope_def_field div_one Nat.cast_pos' NeZero.charZero_one add_sub_cancel_left ConvexOn.slope_le_deriv Set.mem_Ioi Nat.cast_pos add_pos' neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Nat.instAtLeastTwoHAddOfNat ConvexOn.deriv_le_slope Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add le_antisymm ge_of_tendsto instClosedIciTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_harmonic_sub_log Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder le_sub_iff_add_le' sub_eq_add_neg sub_le_iff_le_add' le_of_tendsto tendsto_harmonic_sub_log_add_one neg_neg mul_comm div_eq_iff_mul_eq Nat.factorial_pos Gamma_nat_eq_factorial deriv.log Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq
eulerMascheroniConstant_eq_neg_deriv 📖	mathematical	—	eulerMascheroniConstant Real instNeg deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Gamma instOne	—	CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_add deriv_Gamma_nat Nat.cast_one Rat.cast_zero add_zero mul_neg one_mul neg_neg
hasDerivAt_Gamma_nat 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Gamma instMul instNatCast Nat.factorial instNeg eulerMascheroniConstant instRatCast harmonic instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal DifferentiableAt.hasDerivAt differentiableAt_Gamma Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg sub_eq_zero_of_eq deriv_Gamma_nat
hasDerivAt_Gamma_one 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Gamma instNeg eulerMascheroniConstant instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp Nat.cast_one Rat.cast_zero add_zero mul_neg one_mul Nat.cast_zero zero_add hasDerivAt_Gamma_nat
hasDerivAt_Gamma_one_half 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Gamma instMul instNeg sqrt pi eulerMascheroniConstant instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log DivInvMonoid.toDiv instDivInvMonoid instOne	—	differentiableAt_Gamma LT.lt.ne' LE.le.trans_lt neg_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Nat.cast_nonneg instIsOrderedRing Nat.instAtLeastTwoHAddOfNat DifferentiableAt.comp mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing two_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike DifferentiableAt.const_mul differentiableAt_id HasDerivAt.congr_deriv DifferentiableAt.hasDerivAt one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE deriv_fun_mul one_div instNontrivial HasDerivAt.differentiableAt HasDerivAt.comp_add_const Gamma_one_half_eq add_assoc mul_add Distrib.leftDistribClass deriv_comp_add_const Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo Gamma_one mul_one eulerMascheroniConstant_eq_neg_deriv add_neg_cancel MulZeroClass.mul_zero add_zero Gamma_mul_Gamma_add_half mul_comm deriv_mul_const DifferentiableAt.mul mul_inv_cancel₀ DifferentiableAt.rpow differentiableAt_const DifferentiableAt.const_sub two_ne_zero CharZero.NeZero.two add_mul Distrib.rightDistribClass sub_self rpow_zero one_mul deriv_comp deriv_const_mul mul_one_div div_self deriv_id'' HasDerivAt.deriv hasDerivAt_Gamma_one mul_neg neg_mul ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.rpow hasDerivAt_const IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology HasDerivAt.congr_simp HasDerivAt.const_sub hasDerivAt_mul_const Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Nat.cast_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.natPow_zero Mathlib.Meta.NormNum.IsNat.rpow_eq_pow zero_add Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul

---

← Back to Index