Lemmas

📁 Source: Mathlib/Analysis/Normed/Ring/Lemmas.lean

Statistics

Metric	Count
Definitions mulLeft, mulRight, instNormedCommRing, nonUnitalNormedCommRing, nonUnitalNormedRing, nonUnitalSeminormedCommRing, nonUnitalSeminormedRing, normedCommutativeRing, normedRing, seminormedCommRing, seminormedRing, instNonUnitalNormedCommRing, instNonUnitalNormedRing, instNormedCommRing, instNormedRing	15
Theorems mulLeft_toFun, mulRight_toFun, zero_mul_isBoundedUnder_le, comap_mul_left_cobounded, comap_mul_right_cobounded, isBoundedUnder_le_mul_tendsto_zero, instNormMulClass, instNormOneClass, lipschitzWith_sub, toContinuousMul, toIsTopologicalRing, isometry, inv, instNormOneClass, antilipschitzWith_mul_left, antilipschitzWith_mul_right, tendsto_pow_cobounded_cobounded	17
Total	32

Dilation

Definitions

Name	Category	Theorems
mulLeft 📖	CompOp	1 math math: mulLeft_toFun
mulRight 📖	CompOp	1 math math: mulRight_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulLeft_toFun 📖	mathematical	—	DFunLike.coe Dilation EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NonUnitalNormedRing.toMetricSpace funLike mulLeft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	—
mulRight_toFun 📖	mathematical	—	DFunLike.coe Dilation EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NonUnitalNormedRing.toMetricSpace funLike mulRight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	—

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_mul_left_cobounded 📖	mathematical	—	comap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Bornology.cobounded PseudoMetricSpace.toBornology NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing	—	Dilation.comap_cobounded Dilation.toDilationClass
comap_mul_right_cobounded 📖	mathematical	—	comap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Bornology.cobounded PseudoMetricSpace.toBornology NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing	—	Dilation.comap_cobounded Dilation.toDilationClass
isBoundedUnder_le_mul_tendsto_zero 📖	mathematical	IsBoundedUnder Real Real.instLE Norm.norm NonUnitalSeminormedRing.toNorm Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Tendsto.op_zero_isBoundedUnder_le LE.le.trans_eq norm_mul_le mul_comm

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zero_mul_isBoundedUnder_le 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Filter.IsBoundedUnder Real Real.instLE Norm.norm NonUnitalSeminormedRing.toNorm	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	op_zero_isBoundedUnder_le norm_mul_le

Int

Definitions

Name	Category	Theorems
instNormedCommRing 📖	CompOp	106 math math: ValueDistribution.logCounting_zero, tendsto_zero_iff_meromorphicOrderAt_pos, MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, Function.FactorizedRational.divisor, Function.locallyFinsuppWithin.toClosedBall_support_subset_closedBall, MeromorphicOn.divisor_fun_smul, meromorphicOrderAt_const_ofNat, Padic.withValUniformEquiv_norm_le_one_iff, tendsto_cobounded_iff_meromorphicOrderAt_neg, meromorphicOrderAt_const, Padic.AddValuation.map_one, EisensteinSeries.summand_bound_of_mem_verticalStrip, enorm_natCast, PadicInt.nthHom_zero, padicValuation_lt_one_iff, MeromorphicOn.divisor_const, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, EisensteinSeries.abs_le_right_of_norm, padicValuation_eq_one_iff, MeromorphicOn.divisor_pow, Function.locallyFinsuppWithin.logCounting_eval_zero, MeromorphicOn.divisor_natCast, ValueDistribution.logCounting_top, meromorphicOrderAt_ne_top_iff, MeromorphicOn.divisor_inv, MeromorphicOn.divisor_fun_pow, Function.FactorizedRational.mulSupport, MeromorphicOn.divisor_sub_const_self, MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, meromorphicOrderAt_const_natCast, MeromorphicOn.divisor_intCast, AnalyticAt.meromorphicOrderAt_nonneg, UnitAddTorus.mFourier_zero, MeromorphicOn.divisor_sub_const_of_ne, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, tendsto_nhds_iff_meromorphicOrderAt_nonneg, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, EisensteinSeries.norm_eq_max_natAbs, Function.locallyFinsuppWithin.toClosedBall_divisor, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left, meromorphicNFAt_iff_analyticAt_or, MeromorphicOn.divisor_ofNat, MeromorphicOn.divisor_fun_zpow, MeromorphicOn.divisor_apply, MeromorphicOn.divisor_fun_mul, MeromorphicOn.divisor_zpow, EisensteinSeries.summable_one_div_norm_rpow, toNat_add_toNat_neg_eq_norm, instNormMulClass, tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero, EisensteinSeries.vecMul_SL2_mem_gammaSet, ValueDistribution.characteristic_sub_characteristic_inv, MeromorphicOn.divisor_restrict, EisensteinSeries.isBigO_linear_add_const_vec, EisensteinSeries.r_mul_max_le, EisensteinSeries.norm_symm, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, locallyFinsuppWithin.logCounting_divisor, Matrix.one_le_norm_A_of_ne_zero, MeromorphicOn.divisor_fun_inv, MeromorphicNFOn.zero_set_eq_divisor_support, MeromorphicOn.circleAverage_log_norm, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, MeromorphicOn.AnalyticOnNhd.divisor_nonneg, circleAverage_log_norm_factorizedRational, nnnorm_coe_units, MeromorphicOn.min_divisor_le_divisor_add, meromorphicOrderAt_pow, MeromorphicOn.extract_zeros_poles, MeromorphicOn.negPart_divisor_add_le_max, MeromorphicOn.divisor_smul, EisensteinSeries.abs_le_left_of_norm, nnnorm_natCast, EisensteinSeries.vecMulSL_gcd, EisensteinSeries.abs_norm_eq_max_natAbs, Complex.nnnorm_intCast, meromorphicOrderAt_zpow, Profinite.NobelingProof.CC_comp_zero, norm_coe_units, EisensteinSeries.abs_norm_eq_max_natAbs_neg, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, toNat_add_toNat_neg_eq_nnnorm, MeromorphicOn.negPart_divisor_add_le_add, UnitAddTorus.mFourier_single, Padic.norm_rat_le_one_iff_padicValuation_le_one, NumberField.InfinitePlace.map_intCast, RCLike.instNormSMulClassInt, meromorphicOrderAt_of_not_meromorphicAt, EisensteinSeries.eisSummand_SL2_apply, meromorphicOrderAt_const_intCast, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, MeromorphicOn.divisor_def, padicValuation_le_one, ValueDistribution.logCounting_coe, ValueDistribution.log_counting_zero_sub_logCounting_top, instNormOneClass, MeromorphicOn.divisor_mul, EisensteinSeries.vec_add_const_isTheta, Function.locallyFinsuppWithin.logCounting_even, EisensteinSeries.summand_bound, Matrix.exists_ne_zero_int_vec_norm_le, MeromorphicAt.meromorphicOrderAt_comp, EisensteinSeries.div_max_sq_ge_one, Rat.padicValuation_le_one_iff, Matrix.exists_ne_zero_int_vec_norm_le', Function.locallyFinsuppWithin.toClosedBall_eval_within

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormMulClass 📖	mathematical	—	NormMulClass NormedRing.toNorm NormedCommRing.toNormedRing instNormedCommRing	—	cast_mul abs_mul Real.instIsOrderedRing
instNormOneClass 📖	mathematical	—	NormOneClass NormedRing.toNorm NormedCommRing.toNormedRing instNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing	—	cast_one abs_one Real.instIsOrderedRing

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lipschitzWith_sub 📖	mathematical	—	LipschitzWith NNReal Prod.pseudoEMetricSpaceMax EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace instMetricSpaceNNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat instSub	—	Nat.instAtLeastTwoHAddOfNat Isometry.lipschitzWith_iff isometry_subtype_coe Isometry.prodMap Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Nat.cast_one LipschitzWith.max_const LipschitzWith.sub LipschitzWith.comp LipschitzWith.prod_fst Isometry.lipschitz LipschitzWith.prod_snd

NonUnitalSeminormedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousMul 📖	mathematical	—	ContinuousMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing toNonUnitalRing	—	continuous_iff_continuousAt tendsto_iff_norm_sub_tendsto_zero mul_sub sub_mul sub_add_sub_cancel le_refl norm_add_le_of_le norm_mul_le squeeze_zero norm_nonneg sub_self norm_zero MulZeroClass.mul_zero MulZeroClass.zero_mul add_zero Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul Filter.Tendsto.norm Continuous.tendsto continuous_fst Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_snd tendsto_const_nhds
toIsTopologicalRing 📖	mathematical	—	IsTopologicalRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace NonUnitalRing.toNonUnitalNonAssocRing toNonUnitalRing	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup toContinuousMul IsTopologicalAddGroup.toContinuousNeg

Pi

Definitions

Name	Category	Theorems
nonUnitalNormedCommRing 📖	CompOp	—
nonUnitalNormedRing 📖	CompOp	2 math math: cstarRing', cstarRing
nonUnitalSeminormedCommRing 📖	CompOp	—
nonUnitalSeminormedRing 📖	CompOp	1 math math: Matrix.linfty_opNorm_mulVec
normedCommutativeRing 📖	CompOp	—
normedRing 📖	CompOp	19 math math: NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, EisensteinSeries.summand_bound_of_mem_verticalStrip, NumberField.mixedEmbedding.norm_le_convexBodySumFun, EisensteinSeries.abs_le_right_of_norm, Matrix.l2_opNorm_diagonal, EisensteinSeries.norm_eq_max_natAbs, EisensteinSeries.summable_one_div_norm_rpow, EisensteinSeries.isBigO_linear_add_const_vec, EisensteinSeries.r_mul_max_le, EisensteinSeries.norm_symm, NumberField.canonicalEmbedding.norm_le_iff, EisensteinSeries.abs_le_left_of_norm, EisensteinSeries.abs_norm_eq_max_natAbs, EisensteinSeries.abs_norm_eq_max_natAbs_neg, EisensteinSeries.vec_add_const_isTheta, EisensteinSeries.summand_bound, Int.Matrix.exists_ne_zero_int_vec_norm_le, EisensteinSeries.div_max_sq_ge_one, Int.Matrix.exists_ne_zero_int_vec_norm_le'
seminormedCommRing 📖	CompOp	—
seminormedRing 📖	CompOp	—

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometry 📖	mathematical	—	Isometry PseudoMetricSpace.toPseudoEMetricSpace SeminormedRing.toPseudoMetricSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing instFunLike	—	AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass instRingHomClass RingHomIsometric.norm_map

RingHomIsometric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv 📖	mathematical	—	RingHomIsometric Ring.toSemiring SeminormedRing.toRing SeminormedRing.toNorm	—	norm_map RingHomInvPair.comp_apply_eq₂

SeparationQuotient

Definitions

Name	Category	Theorems
instNonUnitalNormedCommRing 📖	CompOp	—
instNonUnitalNormedRing 📖	CompOp	—
instNormedCommRing 📖	CompOp	—
instNormedRing 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormOneClass 📖	mathematical	—	NormOneClass SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instNorm instOne	—	NormOneClass.norm_one

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitzWith_mul_left 📖	mathematical	—	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NonUnitalNormedRing.toMetricSpace NNReal NNReal.instInv NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	AntilipschitzWith.of_le_mul_dist dist_eq_norm norm_mul inv_mul_cancel_left₀
antilipschitzWith_mul_right 📖	mathematical	—	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NonUnitalNormedRing.toMetricSpace NNReal NNReal.instInv NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	AntilipschitzWith.of_le_mul_dist dist_eq_norm norm_mul mul_comm inv_mul_cancel_left₀
tendsto_pow_cobounded_cobounded 📖	mathematical	—	Filter.Tendsto Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace	—	norm_pow Filter.Tendsto.comp Filter.tendsto_pow_atTop Real.instIsOrderedRing tendsto_norm_cobounded_atTop

---

← Back to Index