Injectivity

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

Statistics

Metric	Count
Definitions	0
Theorems abscissaOfAbsConv_add_le, abscissaOfAbsConv_sub_le, eq_of_LSeries_eventually_eq, tendsto_atTop, tendsto_cpow_mul_atTop, LSeries_eq_iff_of_abscissaOfAbsConv_lt_top, LSeries_eq_zero_iff, LSeries_eq_zero_of_abscissaOfAbsConv_eq_top, LSeries_eventually_eq_zero_iff', LSeries_injOn, LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq	11
Total	11

LSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abscissaOfAbsConv_add_le 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal abscissaOfAbsConv Pi.instAdd Complex Complex.instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal	—	abscissaOfAbsConv_binop_le LSeriesSummable.add
abscissaOfAbsConv_sub_le 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal abscissaOfAbsConv Pi.instSub Complex Complex.instSub SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal	—	abscissaOfAbsConv_binop_le LSeriesSummable.sub
eq_of_LSeries_eventually_eq 📖	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal abscissaOfAbsConv Top.top EReal.instTop Filter.EventuallyEq Real Complex Filter.atTop Real.instPreorder LSeries Complex.ofReal	—	—	LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq lt_top_iff_ne_top LE.le.trans_lt abscissaOfAbsConv_sub_le max_lt LSeries_eventually_eq_zero_iff'
tendsto_atTop 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal abscissaOfAbsConv Top.top EReal.instTop	Filter.Tendsto Real Complex LSeries Complex.ofReal Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	abscissaOfAbsConv_congr LSeries_congr CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero zero_add Complex.one_cpow one_mul tendsto_cpow_mul_atTop
tendsto_cpow_mul_atTop 📖	mathematical	Complex Complex.instZero EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal abscissaOfAbsConv Top.top EReal.instTop	Filter.Tendsto Real Complex.instMul Complex.instPow Complex.instAdd Complex.instNatCast Complex.instOne Complex.ofReal LSeries Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	exists_between instDenselyOrderedEReal CanLift.prf EReal.canLift LT.lt.ne LT.lt.ne' LE.le.trans_lt OrderBot.bot_le Set.indicator_of_notMem not_lt_of_ge lt_trichotomy zero_div MulZeroClass.mul_zero Set.indicator_of_mem LT.lt.trans summable_mul_left_iff IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.natCast_add_one_cpow_ne_zero LSeriesSummable_of_abscissaOfAbsConv_lt_re LT.lt.trans_le EReal.coe_le_coe_iff eq_1 tsum_mul_left Complex.instT2Space Summable.tsum_eq_add_tsum_ite SeminormedAddCommGroup.toIsTopologicalAddGroup pow_mul_term_eq eq_or_ne le_rfl add_zero Filter.Tendsto.congr' Filter.EventuallyEq.symm Filter.eventuallyEq_of_mem Filter.mem_atTop Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd tendsto_const_nhds Summable.congr Summable.indicator SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace lt_or_ge Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg Complex.ofReal_div Complex.ofReal_add div_lt_one Nat.cast_zero RCLike.charZero_rclike div_eq_mul_inv Complex.ofReal_cpow Complex.ofReal_inv Real.inv_rpow inv_div Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul Filter.Tendsto.ofReal tendsto_rpow_atTop_of_base_lt_one neg_one_lt_zero NeZero.charZero_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd T2Space.t1Space Filter.atTop_neBot instIsDirectedOrder Real.instArchimedean tsum_zero tendsto_tsum_of_dominated_convergence Summable.norm Complex.instFiniteDimensionalReal Filter.eventually_iff Filter.mp_mem Filter.univ_mem' norm_div Complex.norm_cpow_real Complex.norm_natCast Nat.cast_add one_le_div Nat.cast_pos' Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono norm_nonneg le_refl Real.rpow_pos_of_pos lt_of_lt_of_le Real.rpow_le_rpow_of_exponent_le norm_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeries_eq_iff_of_abscissaOfAbsConv_lt_top 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal LSeries.abscissaOfAbsConv Top.top EReal.instTop	LSeries	—	LSeries.eq_of_LSeries_eventually_eq Filter.Eventually.of_forall LSeries_congr
LSeries_eq_zero_iff 📖	mathematical	Complex Complex.instZero	LSeries Pi.instZero LSeries.abscissaOfAbsConv Top.top EReal EReal.instTop	—	LSeries_eq_zero_of_abscissaOfAbsConv_eq_top Pi.zero_apply LSeries_eventually_eq_zero_iff' Filter.EventuallyEq.rfl LSeries_zero
LSeries_eq_zero_of_abscissaOfAbsConv_eq_top 📖	mathematical	LSeries.abscissaOfAbsConv Top.top EReal EReal.instTop	LSeries Pi.instZero Complex Complex.instZero	—	LSeries.eq_zero_of_not_LSeriesSummable LSeriesSummable.abscissaOfAbsConv_le LT.lt.false LE.le.trans_lt EReal.coe_lt_top
LSeries_eventually_eq_zero_iff' 📖	mathematical	—	Filter.EventuallyEq Real Complex Filter.atTop Real.instPreorder LSeries Complex.ofReal Pi.instZero Complex.instZero LSeries.abscissaOfAbsConv Top.top EReal EReal.instTop	—	Filter.Eventually.of_forall LSeries_eq_zero_of_abscissaOfAbsConv_eq_top LSeries.abscissaOfAbsConv_congr LSeries_congr Filter.eventuallyEq_iff_exists_mem MulZeroClass.mul_zero Filter.Tendsto.congr' Filter.EventuallyEq.symm T2Space.t1Space Complex.instT2Space Filter.atTop_neBot instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Nat.cast_add Nat.cast_one LSeries.tendsto_cpow_mul_atTop Ne.lt_top LSeries_zero
LSeries_injOn 📖	mathematical	—	Set.InjOn LSeries setOf Complex Complex.instZero EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal LSeries.abscissaOfAbsConv Top.top EReal.instTop	—	LSeries_eq_iff_of_abscissaOfAbsConv_lt_top
LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal LSeries.abscissaOfAbsConv Top.top EReal.instTop Filter.EventuallyEq Real Complex Filter.atTop Real.instPreorder LSeries Complex.ofReal	Pi.instSub Complex.instSub Pi.instZero Complex.instZero	—	Filter.EventuallyEq.eq_1 Filter.eventually_atTop instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean exists_between instDenselyOrderedEReal CanLift.prf EReal.canLift LT.lt.ne LT.lt.ne' LE.le.trans_lt OrderBot.bot_le LSeriesSummable_of_abscissaOfAbsConv_lt_re LT.lt.trans_le EReal.coe_le_coe_iff LE.le.trans le_max_left le_max_right Complex.ofReal_re LSeries_sub sub_self Pi.zero_apply

---

← Back to Index