Deligne

📁 Source: Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean

Statistics

Metric	Count
Definitions Gammaℂ, Gammaℝ	2
Theorems Gammaℂ_add_one, Gammaℂ_def, Gammaℂ_one, Gammaℝ_add_two, Gammaℝ_def, Gammaℝ_div_Gammaℝ_one_sub, Gammaℝ_eq_zero_iff, Gammaℝ_mul_Gammaℝ_add_one, Gammaℝ_ne_zero_of_re_pos, Gammaℝ_one, Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_residue_zero, differentiable_Gammaℝ_inv, inv_Gammaℝ_one_sub, inv_Gammaℝ_two_sub	15
Total	17

Complex

Definitions

Name	Category	Theorems
Gammaℂ 📖	CompOp	10 math math: HurwitzZeta.cosZeta_two_mul_nat', hasDerivAt_Gammaℂ_one, HurwitzZeta.sinZeta_two_mul_nat_add_one', Gammaℂ_def, Gammaℂ_add_one, Gammaℝ_div_Gammaℝ_one_sub, inv_Gammaℝ_one_sub, inv_Gammaℝ_two_sub, Gammaℂ_one, Gammaℝ_mul_Gammaℝ_add_one
Gammaℝ 📖	CompOp	33 math math: hasSum_mellin_pi_mul_sq', HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div, Gammaℝ_def, HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne, hasDerivAt_Gammaℝ_one, ZMod.LFunction_eq_completed_div_gammaFactor_even, HurwitzZeta.hasSum_nat_completedCosZeta, ZetaAsymptotics.tendsto_Gamma_term_aux, Gammaℝ_eq_zero_iff, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, ZMod.LFunction_eq_completed_div_gammaFactor_odd, differentiable_Gammaℝ_inv, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, DirichletCharacter.Even.gammaFactor_def, HurwitzZeta.hasSum_nat_completedSinZeta, Gammaℝ_one, DirichletCharacter.Odd.gammaFactor_def, HurwitzZeta.differentiableAt_update_of_residue, Gammaℝ_residue_zero, Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_add_two, Gammaℝ_div_Gammaℝ_one_sub, riemannZeta_def_of_ne_zero, HurwitzZeta.tendsto_hurwitzZeta_sub_one_div_nhds_one, inv_Gammaℝ_one_sub, HurwitzZeta.hasSum_int_completedCosZeta, HurwitzZeta.hasSum_int_completedSinZeta, HurwitzZeta.hasSum_int_completedHurwitzZetaEven, inv_Gammaℝ_two_sub, Gammaℝ_mul_Gammaℝ_add_one, hasSum_mellin_pi_mul_sq, HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Gammaℂ_add_one 📖	mathematical	—	Gammaℂ Complex instAdd instOne DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat Gammaℂ_def Gamma_add_one neg_add cpow_add mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two instCharZero ofReal_ne_zero Real.pi_ne_zero cpow_neg_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr 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.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf
Gammaℂ_def 📖	mathematical	—	Gammaℂ Complex instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instPow ofReal Real.pi instNeg Gamma	—	—
Gammaℂ_one 📖	mathematical	—	Gammaℂ Complex instOne DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat Gammaℂ_def cpow_neg_one Gamma_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf 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.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Nat.cast_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf
Gammaℝ_add_two 📖	mathematical	—	Gammaℝ Complex instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instMul ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat Gammaℝ_def neg_div add_div neg_add div_self two_ne_zero CharZero.NeZero.two instCharZero Gamma_add_one div_ne_zero cpow_add ofReal_ne_zero Real.pi_ne_zero cpow_neg_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
Gammaℝ_def 📖	mathematical	—	Gammaℝ Complex instMul instPow ofReal Real.pi DivInvMonoid.toDiv instDivInvMonoid instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Gamma	—	—
Gammaℝ_div_Gammaℝ_one_sub 📖	mathematical	—	Complex DivInvMonoid.toDiv instDivInvMonoid Gammaℝ instSub instOne instMul Gammaℂ cos ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg add_comm mul_comm div_div mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass Gammaℝ_one_sub_mul_Gammaℝ_one_add Gammaℝ_mul_Gammaℝ_add_one Gammaℂ_def div_eq_mul_inv inv_inv
Gammaℝ_eq_zero_iff 📖	mathematical	—	Gammaℝ Complex instZero instNeg instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat mul_comm NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass div_eq_iff two_ne_zero' CharZero.NeZero.two instCharZero neg_mul MulZeroClass.zero_mul
Gammaℝ_mul_Gammaℝ_add_one 📖	mathematical	—	Complex instMul Gammaℝ instAdd instOne Gammaℂ	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add mul_one Mathlib.Tactic.RingNF.mul_assoc_rev cpow_add ofReal_ne_zero Real.pi_ne_zero Gamma_mul_Gamma_add_half Real.sqrt_eq_rpow ofReal_cpow LT.lt.le Real.pi_pos ofReal_div ofReal_one ofReal_ofNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf sub_eq_add_neg two_ne_zero CharZero.NeZero.two cpow_one Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat mul_cpow_ofReal_nonneg two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
Gammaℝ_ne_zero_of_re_pos 📖	—	Real Real.instLT Real.instZero re	—	—	mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass instCharZero Gamma_ne_zero_of_re_pos div_ofNat_re div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
Gammaℝ_one 📖	mathematical	—	Gammaℝ Complex instOne	—	Nat.instAtLeastTwoHAddOfNat Gammaℝ_def Gamma_one_half_eq neg_div one_div cpow_neg inv_mul_cancel₀ instCharZero
Gammaℝ_one_sub_mul_Gammaℝ_one_add 📖	mathematical	—	Complex instMul Gammaℝ instSub instOne instAdd instInv cos DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast add_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_congr mul_one Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isRat_add Gamma_mul_Gamma_one_sub cpow_one Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat cpow_add ofReal_ne_zero Real.pi_ne_zero sin_pi_div_two_sub Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.inv_congr cpow_zero one_mul
Gammaℝ_residue_zero 📖	mathematical	—	Filter.Tendsto Complex instMul Gammaℝ nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero Compl.compl Set Set.instCompl Set.instSingletonSet nhds instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Filter.Tendsto.comp tendsto_self_mul_Gamma_nhds_zero tendsto_nhdsWithin_iff zero_div Filter.Tendsto.mono_left Filter.Tendsto.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Filter.tendsto_id nhdsWithin_le_nhds Filter.eventually_of_mem self_mem_nhdsWithin div_ne_zero two_ne_zero CharZero.NeZero.two instCharZero neg_zero cpow_zero mul_one ContinuousAt.tendsto ContinuousAt.mul continuousAt_const ContinuousAt.comp continuousAt_const_cpow ofReal_ne_zero Real.pi_ne_zero ContinuousAt.comp' Continuous.continuousAt Continuous.div_const continuous_id' ContinuousAt.neg IsTopologicalRing.toContinuousNeg continuousAt_id' Gammaℝ.eq_1 Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Filter.Tendsto.mul
differentiable_Gammaℝ_inv 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instInv Gammaℝ	—	Gammaℝ.eq_1 mul_inv Differentiable.mul DifferentiableAt.inv DifferentiableAt.const_cpow Nat.instAtLeastTwoHAddOfNat DifferentiableAt.div_const DifferentiableAt.neg differentiableAt_id ofReal_ne_zero Real.pi_ne_zero instCharZero Differentiable.comp differentiable_one_div_Gamma Differentiable.div_const differentiable_id
inv_Gammaℝ_one_sub 📖	mathematical	—	Complex instInv Gammaℝ instSub instOne instMul Gammaℂ cos DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Gammaℝ_eq_zero_iff Nat.cast_mul neg_add_rev Nat.cast_add Nat.cast_one Gammaℝ_div_Gammaℝ_one_sub div_eq_mul_inv div_right_comm div_self one_div
inv_Gammaℝ_two_sub 📖	mathematical	—	Complex instInv Gammaℝ instSub instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instMul Gammaℂ sin DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi instAdd instOne	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Tactic.Ring.sub_pf 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 Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Gammaℝ_one Gammaℝ.eq_1 neg_div add_self_div_two CharZero.NeZero.two instCharZero Gamma_one Gammaℂ_one mul_one sin_pi_div_two cpow_neg_one inv_inv div_mul_cancel₀ ofReal_ne_zero Real.pi_ne_zero inv_one Nat.cast_zero neg_zero sub_ne_zero sub_eq_iff_eq_add Nat.cast_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.isNat_add inv_Gammaℝ_one_sub sub_add_cancel Gammaℂ_add_one Gammaℝ_add_two mul_sub sub_div cos_sub_pi_div_two mul_div_assoc mul_inv Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.mul_congr 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.zero_mul

---

← Back to Index