Mathlib Map

Theorems · Theorem · special functions

Complex.not_continuousAt_Gamma_zero

¬ContinuousAt Complex.Gamma 0
Defined in
Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Cited by
2 results in Mathlib
Foundations
Depth 287 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Complex.not_continuousAt_Gamma_neg_nat · cited by 1Complex.not_continuousAt_…Complex.not_differentiableAt_Gamma_zero · cited by 1Complex.not_differentiabl…Complex · cited by 5565Complexnhds · cited by 5554nhdsDisjoint · cited by 2201DisjointMulZeroClass.mul_zero · cited by 2091MulZeroClass.mul_zeroContinuousAt · cited by 697ContinuousAtComplex.Gamma · cited by 96Complex.GammacontinuousAt_id · cited by 28continuousAt_idFilter.Tendsto.not_tendsto · cited by 14Tendsto.not_tendstoContinuousAt.mul · cited by 14ContinuousAt.mulComplex.Gamma_zero · cited by 7Complex.Gamma_zerocontinuousAt_iff_punctured_nhds · cited by 4continuousAt_iff_puncture…Complex.tendsto_self_mul_Gamma_nhds_zero · cited by 2Complex.tendsto_self_mul_…Complex.not_continuousAt_Gamm…CITED BYCITES

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.