DedekindZeta

📁 Source: Mathlib/NumberTheory/NumberField/DedekindZeta.lean

Statistics

Metric	Count
Definitions dedekindZeta, dedekindZeta_residue	2
Theorems dedekindZeta_residue_def, dedekindZeta_residue_ne_zero, dedekindZeta_residue_pos, tendsto_sub_one_mul_dedekindZeta_nhdsGT	4
Total	6

NumberField

Definitions

Name	Category	Theorems
dedekindZeta 📖	CompOp	1 math math: tendsto_sub_one_mul_dedekindZeta_nhdsGT
dedekindZeta_residue 📖	CompOp	3 math math: dedekindZeta_residue_def, tendsto_sub_one_mul_dedekindZeta_nhdsGT, dedekindZeta_residue_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dedekindZeta_residue_def 📖	mathematical	—	dedekindZeta_residue Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat InfinitePlace.nrRealPlaces Real.pi InfinitePlace.nrComplexPlaces Units.regulator classNumber Units.torsionOrder Real.sqrt abs Real.lattice Real.instAddGroup Real.instIntCast discr	—	—
dedekindZeta_residue_ne_zero 📖	—	—	—	—	LT.lt.ne' dedekindZeta_residue_pos
dedekindZeta_residue_pos 📖	mathematical	—	Real Real.instLT Real.instZero dedekindZeta_residue	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Units.regulator_pos Nat.cast_pos classNumber_pos Units.torsionOrder_pos Real.sqrt_pos_of_pos abs_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Int.cast_ne_zero RCLike.charZero_rclike discr_ne_zero
tendsto_sub_one_mul_dedekindZeta_nhdsGT 📖	mathematical	—	Filter.Tendsto Real Complex Complex.instMul Complex.instSub Complex.ofReal Complex.instOne dedekindZeta nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne Set.Ioi Real.instPreorder nhds SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField dedekindZeta_residue	—	LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg RingOfIntegers.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt Filter.Tendsto.congr IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike AddRightCancelSemigroup.toIsRightCancelAdd Ideal.card_norm_le_eq_card_norm_le_add_one Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt RingOfIntegers.instCharZero_1 to_charZero Finset.Icc_succ_left_eq_Ioc Nat.instNoMaxOrder Nat.card_eq_fintype_card Fintype.card_unique Finset.sum_Ioc_add_eq_sum_Icc Finset.card_preimage_eq_sum_card_image_eq Ideal.finite_setOf_absNorm_eq Finset.coe_Icc Nat.instCanonicallyOrderedAdd Filter.Tendsto.comp Nat.instAtLeastTwoHAddOfNat Ideal.tendsto_norm_le_div_atTop₀ tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean Nat.cast_nonneg

---

← Back to Index