Exponential

📁 Source: Mathlib/Analysis/Normed/Algebra/Exponential.lean

Statistics

Metric	Count
Definitions exp, expSeries, invertibleExp, invertibleExpOfMemBall	4
Theorems exp, exp_left, exp_right, exp, update_exp, exp, algebraMap_exp_comm, algebraMap_exp_comm_of_mem_ball, analyticAt_exp_of_mem_ball, continuousOn_exp, expSeries_apply_eq, expSeries_apply_eq', expSeries_apply_eq_div, expSeries_apply_eq_div', expSeries_apply_zero, expSeries_div_hasSum_exp, expSeries_div_hasSum_exp_of_mem_ball, expSeries_div_summable, expSeries_div_summable_of_mem_ball, expSeries_eq_expSeries, expSeries_eq_expSeries_rat, expSeries_eq_ofScalars, expSeries_hasSum_exp, expSeries_hasSum_exp_of_mem_ball, expSeries_hasSum_exp_of_mem_ball', expSeries_radius_eq_top, expSeries_radius_pos, expSeries_sum_eq, expSeries_sum_eq_div, expSeries_sum_eq_rat, expSeries_summable, expSeries_summable', expSeries_summable_of_mem_ball, expSeries_summable_of_mem_ball', exp_add, exp_add_of_commute, exp_add_of_commute_of_mem_ball, exp_add_of_mem_ball, exp_analytic, exp_conj, exp_conj', exp_continuous, exp_def, exp_eq_expSeries_sum, exp_eq_ofScalarsSum, exp_eq_tsum, exp_eq_tsum_div, exp_eq_tsum_rat, exp_hasFPowerSeriesAt_zero, exp_hasFPowerSeriesOnBall, exp_mem_unitary_of_mem_skewAdjoint, exp_neg, exp_neg_of_mem_ball, exp_nsmul, exp_op, exp_series_hasSum_exp', exp_smul, exp_sum, exp_sum_of_commute, exp_units_conj, exp_units_conj', exp_unop, exp_zero, exp_zsmul, hasFPowerSeriesAt_exp_zero_of_radius_pos, hasFPowerSeriesOnBall_exp_of_radius_pos, invOf_exp, invOf_exp_of_mem_ball, isUnit_exp, isUnit_exp_of_mem_ball, map_exp, map_exp_of_mem_ball, norm_expSeries_div_summable, norm_expSeries_div_summable_of_mem_ball, norm_expSeries_summable, norm_expSeries_summable', norm_expSeries_summable_of_mem_ball, norm_expSeries_summable_of_mem_ball', ofReal_exp_ℝ_ℝ, of_real_exp_ℝ_ℝ, star_exp, coe_exp, exp_def, fst_exp, snd_exp, inverse_exp	86
Total	90

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	NormedSpace.exp	—	exp_right exp_left
exp_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	NormedSpace.exp	—	symm exp_right
exp_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	NormedSpace.exp	—	NormedSpace.exp_eq_tsum Rat.instCharZero tsum_right IsTopologicalRing.toIsTopologicalSemiring SummationFilter.instNeBotUnconditional smul_right Algebra.to_smulCommClass IsScalarTower.right pow_right NormedSpace.exp_def one_right

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	NormedSpace.exp NormedRing.toRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	comp NonUnitalSeminormedRing.toIsTopologicalRing Continuous.tendsto NormedSpace.exp_continuous

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
update_exp 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	update NormedSpace.exp Pi.ring NormedRing.toRing Pi.topologicalSpace UniformSpace.toTopologicalSpace Pi.instIsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	Pi.instIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing update.congr_simp Pi.exp_def apply_update

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	NormedSpace.exp	—	NormedSpace.star_exp

NormedSpace

Definitions

Name	Category	Theorems
exp 📖	CompOp	139 math math: Commute.exp_right, HasSum.exp, exp_neg_of_mem_ball, exp_continuous, TrivSqZeroExt.exp_inr, Matrix.IsSymm.exp, hasStrictFDerivAt_exp_of_mem_ball, hasFPowerSeriesAt_exp_zero_of_radius_pos, exp_zsmul, Filter.Tendsto.exp, invOf_exp_of_mem_ball, hasDerivAt_exp_zero_of_radius_pos, isUnit_exp_of_mem_ball, CFC.exp_log, Complex.exp_eq_exp_ℂ, exp_series_hasSum_exp', hasStrictFDerivAt_exp_smul_const_of_mem_ball', Matrix.exp_conj', Matrix.exp_neg, TrivSqZeroExt.fst_exp, Function.update_exp, map_exp, Commute.exp_left, exp_hasFPowerSeriesOnBall, hasStrictDerivAt_exp_smul_const, exp_eq_tsum, hasStrictDerivAt_exp_smul_const', exp_eq_tsum_div, Matrix.exp_add_of_commute, TrivSqZeroExt.eq_smul_exp_of_ne_zero, hasStrictFDerivAt_exp, exp_conj, Commute.exp, Matrix.IsHermitian.exp, expSeries_hasSum_exp, hasStrictFDerivAt_exp_smul_const', analyticAt_exp_of_mem_ball, TrivSqZeroExt.snd_exp, IsSelfAdjoint.exp, exp_continuousMap_eq, Matrix.exp_diagonal, hasFPowerSeriesOnBall_exp_of_radius_pos, Matrix.exp_nsmul, CFC.exp_eq_normedSpace_exp, hasFDerivAt_exp_smul_const', Quaternion.exp_of_re_eq_zero, Matrix.exp_zsmul, expSeries_div_hasSum_exp_of_mem_ball, Matrix.exp_sum_of_commute, exp_op, Quaternion.re_exp, ofReal_exp_ℝ_ℝ, star_exp, exp_add_of_commute_of_mem_ball, Matrix.exp_conjTranspose, hasDerivAt_exp_smul_const, algebraMap_exp_comm, map_exp_of_mem_ball, Matrix.exp_transpose, exp_sum, invOf_exp, DualNumber.exp_eps, exp_conj', exp_units_conj', hasDerivAt_exp, exp_zero, TrivSqZeroExt.exp_def, Quaternion.normSq_exp, IsSelfAdjoint.exp_nonneg, exp_hasFPowerSeriesAt_zero, Quaternion.im_exp, exp_nsmul, hasFDerivAt_exp_zero, hasFDerivAt_exp_smul_const_of_mem_ball, Matrix.exp_conj, exp_def, hasFDerivAt_exp_smul_const, Prod.fst_exp, Matrix.exp_blockDiagonal, Matrix.exp_units_conj', hasStrictFDerivAt_exp_zero_of_radius_pos, hasStrictFDerivAt_exp_zero, Quaternion.norm_exp, spectrum.exp_mem_exp, exp_neg, exp_smul, hasDerivAt_exp_smul_const_of_mem_ball', of_real_exp_ℝ_ℝ, expSeries_div_hasSum_exp, hasStrictDerivAt_exp, continuousOn_exp, Matrix.isUnit_exp, TrivSqZeroExt.exp_inl, hasStrictDerivAt_exp_zero_of_radius_pos, DualNumber.exp_smul_eps, hasStrictDerivAt_exp_of_mem_ball, algebraMap_exp_comm_of_mem_ball, hasStrictDerivAt_exp_smul_const_of_mem_ball', hasFDerivAt_exp_smul_const_of_mem_ball', hasStrictFDerivAt_exp_smul_const, exp_eq_tsum_rat, hasDerivAt_exp_smul_const', TrivSqZeroExt.exp_def_of_smul_comm, exp_add_of_commute, Prod.snd_exp, Real.exp_eq_exp_ℝ, isUnit_exp, Matrix.exp_blockDiagonal', expSeries_hasSum_exp_of_mem_ball', hasFDerivAt_exp_zero_of_radius_pos, CFC.log_exp, hasDerivAt_exp_zero, exp_add_of_mem_ball, exp_analytic, exp_sum_of_commute, hasDerivAt_exp_of_mem_ball, hasStrictDerivAt_exp_smul_const_of_mem_ball, Matrix.exp_units_conj, exp_units_conj, exp_mem_unitary_of_mem_skewAdjoint, hasFDerivAt_exp, CFC.real_exp_eq_normedSpace_exp, Ring.inverse_exp, hasDerivAt_exp_smul_const_of_mem_ball, hasStrictDerivAt_exp_zero, expSeries_hasSum_exp_of_mem_ball, CFC.complex_exp_eq_normedSpace_exp, Quaternion.exp_coe, hasFDerivAt_exp_of_mem_ball, Quaternion.exp_eq, exp_unop, Pi.exp_def, TrivSqZeroExt.eq_smul_exp_of_invertible, selfAdjoint.expUnitary_coe, hasStrictFDerivAt_exp_smul_const_of_mem_ball, exp_add, exp_eq_expSeries_sum, Pi.coe_exp, exp_eq_ofScalarsSum
expSeries 📖	CompOp	26 math math: expSeries_eq_ofScalars, expSeries_apply_eq_div', exp_hasFPowerSeriesOnBall, expSeries_eq_expSeries, expSeries_summable, TrivSqZeroExt.fst_expSeries, norm_expSeries_summable, expSeries_sum_eq, expSeries_hasSum_exp, Quaternion.expSeries_odd_of_imaginary, expSeries_apply_eq, Quaternion.expSeries_even_of_imaginary, expSeries_apply_eq_div, expSeries_radius_eq_top, expSeries_apply_zero, exp_hasFPowerSeriesAt_zero, expSeries_apply_eq', expSeries_sum_eq_rat, exp_def, expSeries_sum_eq_div, expSeries_eq_expSeries_rat, continuousOn_exp, expSeries_radius_pos, Quaternion.hasSum_expSeries_of_imaginary, TrivSqZeroExt.snd_expSeries_of_smul_comm, exp_eq_expSeries_sum
invertibleExp 📖	CompOp	—
invertibleExpOfMemBall 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_exp_comm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring NormedRing.toRing RingHom.instFunLike algebraMap NormedAlgebra.toAlgebra NormedRing.toSeminormedRing exp NormedCommRing.toNormedRing NormedField.toNormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	algebraMap_exp_comm_of_mem_ball edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top
algebraMap_exp_comm_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedField.toNormedSpace expSeries NormedField.toField NormedRing.toRing NormedCommRing.toNormedRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap NormedAlgebra.toAlgebra NormedRing.toSeminormedRing exp NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing map_exp_of_mem_ball RingHom.instRingHomClass ContinuousLinearMap.continuous IsBoundedSMul.continuousSMul toIsBoundedSMul
analyticAt_exp_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	AnalyticAt exp	—	NonUnitalSeminormedRing.toIsTopologicalRing ENNReal.not_lt_zero pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd HasFPowerSeriesOnBall.analyticAt_of_mem hasFPowerSeriesOnBall_exp_of_radius_pos
continuousOn_exp 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing exp NormedRing.toRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField expSeries NormedField.toField NormedAlgebra.toAlgebra	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul toIsBoundedSMul NonUnitalSeminormedRing.toIsTopologicalRing FormalMultilinearSeries.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul exp_eq_expSeries_sum
expSeries_apply_eq 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries Algebra.toSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	List.ofFn_const List.prod_replicate
expSeries_apply_eq' 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries Algebra.toSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	expSeries_apply_eq
expSeries_apply_eq_div 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial	—	div_eq_mul_inv Commute.eq Commute.inv_left₀ Nat.cast_commute smul_eq_mul expSeries_apply_eq inv_natCast_smul_eq
expSeries_apply_eq_div' 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial	—	expSeries_apply_eq_div
expSeries_apply_zero 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	expSeries_apply_eq pow_zero Nat.factorial_zero Nat.cast_one inv_one one_smul Pi.single_eq_same zero_pow smul_zero Pi.single_eq_of_ne
expSeries_div_hasSum_exp 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing Nat.factorial exp IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SummationFilter.unconditional	—	expSeries_div_hasSum_exp_of_mem_ball Rat.instCharZero edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
expSeries_div_hasSum_exp_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedDivisionRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial exp SummationFilter.unconditional	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing expSeries_apply_eq_div' expSeries_hasSum_exp_of_mem_ball
expSeries_div_summable 📖	mathematical	—	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing Nat.factorial SummationFilter.unconditional	—	Summable.of_norm norm_expSeries_div_summable
expSeries_div_summable_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedDivisionRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	Summable ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial SummationFilter.unconditional	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Summable.of_norm norm_expSeries_div_summable_of_mem_ball
expSeries_eq_expSeries 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries	—	expSeries_apply_eq inv_natCast_smul_eq
expSeries_eq_expSeries_rat 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike expSeries Rat.instField	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul SMulCommClass.rat' inv_natCast_smul_eq smulCommClass_self
expSeries_eq_ofScalars 📖	mathematical	—	expSeries FormalMultilinearSeries.ofScalars InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul
expSeries_hasSum_exp 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring NormedAlgebra.toAlgebra ContinuousMultilinearMap.funLike expSeries NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing exp SummationFilter.unconditional	—	expSeries_hasSum_exp_of_mem_ball edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top
expSeries_hasSum_exp_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike exp SummationFilter.unconditional	—	NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul exp_eq_expSeries_sum FormalMultilinearSeries.hasSum
expSeries_hasSum_exp_of_mem_ball' 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring SeminormedRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing NormedField.toNormedCommRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero exp SummationFilter.unconditional	—	NonUnitalSeminormedRing.toIsTopologicalRing expSeries_apply_eq' expSeries_hasSum_exp_of_mem_ball
expSeries_radius_eq_top 📖	mathematical	—	FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing Top.top ENNReal instTopENNReal	—	Nat.cast_ne_zero Nat.factorial_ne_zero IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul FormalMultilinearSeries.ofScalars_radius_eq_top_of_tendsto Filter.Eventually.of_forall expSeries_eq_ofScalars Nat.cast_mul mul_inv_rev mul_div_right_comm inv_div_inv norm_mul NormedDivisionRing.toNormMulClass div_self NormOneClass.norm_one NormedDivisionRing.to_normOneClass one_mul Filter.Tendsto.norm norm_zero Filter.tendsto_add_atTop_iff_nat tendsto_inv_atTop_nhds_zero_nat NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero
expSeries_radius_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	—	NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top WithTop.top_pos
expSeries_sum_eq 📖	mathematical	—	FormalMultilinearSeries.sum DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring expSeries tsum Algebra.toSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Monoid.toNatPow SummationFilter.unconditional	—	tsum_congr expSeries_apply_eq
expSeries_sum_eq_div 📖	mathematical	—	FormalMultilinearSeries.sum DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring expSeries tsum DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial SummationFilter.unconditional	—	tsum_congr expSeries_apply_eq_div
expSeries_sum_eq_rat 📖	mathematical	—	FormalMultilinearSeries.sum DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring expSeries Rat.instField	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul expSeries_sum_eq inv_natCast_smul_eq
expSeries_summable 📖	mathematical	—	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring NormedAlgebra.toAlgebra ContinuousMultilinearMap.funLike expSeries NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing SummationFilter.unconditional	—	Summable.of_norm NonUnitalSeminormedRing.toIsTopologicalRing norm_expSeries_summable
expSeries_summable' 📖	mathematical	—	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	Summable.of_norm norm_expSeries_summable'
expSeries_summable_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	Summable ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike SummationFilter.unconditional	—	NonUnitalSeminormedRing.toIsTopologicalRing Summable.of_norm norm_expSeries_summable_of_mem_ball
expSeries_summable_of_mem_ball' 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	Summable ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring SeminormedRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing NormedField.toNormedCommRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	NonUnitalSeminormedRing.toIsTopologicalRing Summable.of_norm norm_expSeries_summable_of_mem_ball'
exp_add 📖	mathematical	—	exp NormedRing.toRing NormedCommRing.toNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Distrib.toMul	—	exp_add_of_mem_ball Rat.instCharZero edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
exp_add_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Distrib.toAdd	—	exp_add_of_commute_of_mem_ball Rat.instCharZero edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
exp_add_of_commute_of_mem_ball 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	exp Distrib.toAdd	—	NonUnitalSeminormedRing.toIsTopologicalRing exp_eq_tsum tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm norm_expSeries_summable_of_mem_ball' Commute.add_pow' Finset.smul_sum tsum_congr Finset.sum_congr Nat.cast_smul_eq_nsmul smul_smul smul_mul_smul_comm IsScalarTower.right IsScalarTower.left Algebra.to_smulCommClass Finset.HasAntidiagonal.mem_antidiagonal Nat.cast_add_choose Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Nat.factorial_ne_zero Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one
exp_add_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing expSeries NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	exp Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	—	NonUnitalSeminormedRing.toIsTopologicalRing exp_add_of_commute_of_mem_ball Commute.all
exp_analytic 📖	mathematical	—	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	—	analyticAt_exp_of_mem_ball edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top
exp_conj 📖	mathematical	—	exp NormedRing.toRing NormedDivisionRing.toNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	exp_units_conj
exp_conj' 📖	mathematical	—	exp NormedRing.toRing NormedDivisionRing.toNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	exp_units_conj'
exp_continuous 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing exp NormedRing.toRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	NonUnitalSeminormedRing.toIsTopologicalRing continuousOn_univ Metric.eball_top_eq_univ expSeries_radius_eq_top Rat.instCharZero ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing continuousOn_exp
exp_def 📖	mathematical	—	exp Algebra Rat.commSemiring Ring.toSemiring FormalMultilinearSeries.sum DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Rat.instField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Nonempty.some expSeries AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
exp_eq_expSeries_sum 📖	mathematical	—	exp FormalMultilinearSeries.sum DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring expSeries	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul exp_def expSeries_sum_eq_rat
exp_eq_ofScalarsSum 📖	mathematical	—	exp FormalMultilinearSeries.ofScalarsSum InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial	—	exp_eq_tsum FormalMultilinearSeries.ofScalarsSum_eq_tsum
exp_eq_tsum 📖	mathematical	—	exp tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul exp_eq_expSeries_sum expSeries_sum_eq
exp_eq_tsum_div 📖	mathematical	—	exp DivisionRing.toRing tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial SummationFilter.unconditional	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul exp_eq_expSeries_sum Rat.instCharZero expSeries_sum_eq_div
exp_eq_tsum_rat 📖	mathematical	—	exp tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Rat.commSemiring Ring.toSemiring Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	exp_eq_tsum Rat.instCharZero
exp_hasFPowerSeriesAt_zero 📖	mathematical	—	HasFPowerSeriesAt NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	HasFPowerSeriesOnBall.hasFPowerSeriesAt NonUnitalSeminormedRing.toIsTopologicalRing exp_hasFPowerSeriesOnBall
exp_hasFPowerSeriesOnBall 📖	mathematical	—	HasFPowerSeriesOnBall NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top ENNReal instTopENNReal	—	NonUnitalSeminormedRing.toIsTopologicalRing hasFPowerSeriesOnBall_exp_of_radius_pos expSeries_radius_pos expSeries_radius_eq_top
exp_mem_unitary_of_mem_skewAdjoint 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing SetLike.instMembership AddSubgroup.instSetLike skewAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	—	NonUnitalSeminormedRing.toIsTopologicalRing Unitary.mem_iff star_exp TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace skewAdjoint.mem_iff exp_add_of_commute Commute.neg_left Commute.refl Commute.neg_right neg_add_cancel add_neg_cancel exp_zero
exp_neg 📖	mathematical	—	exp NormedRing.toRing NormedDivisionRing.toNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	exp_neg_of_mem_ball Rat.instCharZero edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
exp_neg_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedDivisionRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	exp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing invOf_eq_inv
exp_nsmul 📖	mathematical	—	exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	NonUnitalSeminormedRing.toIsTopologicalRing zero_smul pow_zero exp_zero succ_nsmul pow_succ exp_add_of_commute Commute.smul_left Algebra.to_smulCommClass IsScalarTower.right Commute.refl
exp_op 📖	mathematical	—	exp MulOpposite MulOpposite.instRing MulOpposite.instTopologicalSpaceMulOpposite instIsTopologicalRingMulOpposite NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulOpposite.op	—	instIsTopologicalRingMulOpposite exp_eq_tsum Rat.instCharZero tsum_op exp_def MulOpposite.op_one
exp_series_hasSum_exp' 📖	mathematical	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero exp NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing SummationFilter.unconditional	—	expSeries_hasSum_exp_of_mem_ball' edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top
exp_smul 📖	mathematical	—	exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	NonUnitalSeminormedRing.toIsTopologicalRing map_exp RingHom.instRingHomClass ContinuousConstSMul.continuous_const_smul
exp_sum 📖	mathematical	—	exp NormedRing.toRing NormedCommRing.toNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Finset.prod CommRing.toCommMonoid NormedCommRing.toCommRing	—	NonUnitalSeminormedRing.toIsTopologicalRing Commute.exp TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Pairwise.of_refl Commute.on_refl Commute.all exp_sum_of_commute Finset.noncommProd_eq_prod
exp_sum_of_commute 📖	mathematical	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup Finset.noncommProd MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Commute.exp TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace Set.Pairwise.of_refl Commute.on_refl	—	Finset.induction_on NonUnitalSeminormedRing.toIsTopologicalRing Commute.exp TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Pairwise.of_refl Commute.on_refl exp_zero Set.Pairwise.mono Finset.mem_insert_of_mem Finset.noncommProd_insert_of_notMem Finset.sum_insert exp_add_of_commute Commute.sum_right Finset.mem_insert_self Finset.subset_insert
exp_units_conj 📖	mathematical	—	exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	exp_smul ConjAct.units_continuousConstSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing
exp_units_conj' 📖	mathematical	—	exp NormedRing.toRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	exp_units_conj
exp_unop 📖	mathematical	—	exp MulOpposite.unop MulOpposite MulOpposite.instRing MulOpposite.instTopologicalSpaceMulOpposite instIsTopologicalRingMulOpposite NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	instIsTopologicalRingMulOpposite exp_op
exp_zero 📖	mathematical	—	exp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	exp_def expSeries_sum_eq expSeries_apply_zero tsum_pi_single
exp_zsmul 📖	mathematical	—	exp NormedRing.toRing NormedDivisionRing.toNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing zpow_natCast natCast_zsmul NonUnitalSeminormedRing.toIsTopologicalRing exp_nsmul zpow_neg neg_smul exp_neg
hasFPowerSeriesAt_exp_zero_of_radius_pos 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	HasFPowerSeriesAt exp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	NonUnitalSeminormedRing.toIsTopologicalRing HasFPowerSeriesOnBall.hasFPowerSeriesAt hasFPowerSeriesOnBall_exp_of_radius_pos
hasFPowerSeriesOnBall_exp_of_radius_pos 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	HasFPowerSeriesOnBall exp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul toIsBoundedSMul exp_eq_expSeries_sum FormalMultilinearSeries.hasFPowerSeriesOnBall
invOf_exp 📖	mathematical	—	Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup	—	NonUnitalSeminormedRing.toIsTopologicalRing invOf_exp_of_mem_ball Rat.instCharZero edist_lt_top expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
invOf_exp_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne exp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	NonUnitalSeminormedRing.toIsTopologicalRing Invertible.congr
isUnit_exp 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	isUnit_exp_of_mem_ball Rat.instCharZero edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
isUnit_exp_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring exp	—	NonUnitalSeminormedRing.toIsTopologicalRing isUnit_of_invertible
map_exp 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing DFunLike.coe	exp NormedRing.toRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	map_exp_of_mem_ball Rat.instCharZero edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
map_exp_of_mem_ball 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing DFunLike.coe Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField expSeries NormedField.toField NormedAlgebra.toAlgebra NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	exp	—	NonUnitalSeminormedRing.toIsTopologicalRing exp_eq_tsum HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional HasSum.map Summable.hasSum expSeries_summable_of_mem_ball' RingHomClass.toAddMonoidHomClass map_inv_natCast_smul map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
norm_expSeries_div_summable 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedDivisionRing.toNorm DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedDivisionRing.toNormedRing Nat.factorial SummationFilter.unconditional	—	norm_expSeries_div_summable_of_mem_ball edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top Rat.instCharZero ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Rat.instIsTopologicalRing
norm_expSeries_div_summable_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedDivisionRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	Summable Real Real.instAddCommMonoid Real.pseudoMetricSpace Norm.norm NormedDivisionRing.toNorm DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial SummationFilter.unconditional	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing expSeries_apply_eq_div' norm_expSeries_summable_of_mem_ball
norm_expSeries_summable 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring NormedAlgebra.toAlgebra NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace ContinuousMultilinearMap.funLike expSeries NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing SummationFilter.unconditional	—	norm_expSeries_summable_of_mem_ball edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top
norm_expSeries_summable' 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing NormedRing.toSeminormedRing NormedAlgebra.toAlgebra InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	norm_expSeries_summable_of_mem_ball' edist_lt_top NonUnitalSeminormedRing.toIsTopologicalRing expSeries_radius_eq_top
norm_expSeries_summable_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	Summable Real Real.instAddCommMonoid Real.pseudoMetricSpace Norm.norm NormedRing.toNorm DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike SummationFilter.unconditional	—	NonUnitalSeminormedRing.toIsTopologicalRing FormalMultilinearSeries.summable_norm_apply
norm_expSeries_summable_of_mem_ball' 📖	mathematical	Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing FormalMultilinearSeries.radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing expSeries NormedField.toField NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	Summable Real Real.instAddCommMonoid Real.pseudoMetricSpace Norm.norm NormedRing.toNorm Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring SeminormedRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing NormedField.toNormedCommRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	NonUnitalSeminormedRing.toIsTopologicalRing expSeries_apply_eq' norm_expSeries_summable_of_mem_ball
ofReal_exp_ℝ_ℝ 📖	mathematical	—	Complex.ofReal exp Real Real.instRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalRingReal Complex Complex.instRing SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	—	map_exp RCLike.charZero_rclike Real.instCompleteSpace Complex.instCharZero RingHom.instRingHomClass continuous_algebraMap IsBoundedSMul.continuousSMul toIsBoundedSMul
of_real_exp_ℝ_ℝ 📖	mathematical	—	Complex.ofReal exp Real Real.instRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalRingReal Complex Complex.instRing SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	—	ofReal_exp_ℝ_ℝ
star_exp 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid exp	—	exp_eq_tsum Rat.instCharZero exp_def star_one

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_exp 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	NormedSpace.exp ring NormedRing.toRing topologicalSpace UniformSpace.toTopologicalSpace instIsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	instIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing nonempty_fintype NormedSpace.map_exp complete RingHom.instRingHomClass continuous_apply
exp_def 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	NormedSpace.exp ring NormedRing.toRing topologicalSpace UniformSpace.toTopologicalSpace instIsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	instIsTopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing coe_exp

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_exp 📖	mathematical	—	NormedSpace.exp instRing NormedRing.toRing instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instIsTopologicalRingProd NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	NormedSpace.map_exp CompleteSpace.prod RingHom.instRingHomClass continuous_fst
snd_exp 📖	mathematical	—	NormedSpace.exp instRing NormedRing.toRing instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instIsTopologicalRingProd NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	NormedSpace.map_exp CompleteSpace.prod RingHom.instRingHomClass continuous_snd

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_exp 📖	mathematical	—	inverse Semiring.toMonoidWithZero toSemiring NormedRing.toRing NormedSpace.exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup	—	inverse_invertible NonUnitalSeminormedRing.toIsTopologicalRing

---

← Back to Index