OfScalars

📁 Source: Mathlib/Analysis/Analytic/OfScalars.lean

Statistics

Metric	Count
Definitions ofScalars, ofScalarsSubmodule, ofScalarsSum	3
Theorems coeff_ofScalars, inv_le_ofScalars_radius_of_tendsto, ofScalarsSum_eq_tsum, ofScalarsSum_of_subsingleton, ofScalarsSum_op, ofScalarsSum_unop, ofScalarsSum_zero, ofScalars_add, ofScalars_apply_eq, ofScalars_apply_eq', ofScalars_apply_zero, ofScalars_comp_neg, ofScalars_comp_neg_id, ofScalars_eq_zero, ofScalars_eq_zero_of_scalar_zero, ofScalars_norm, ofScalars_norm_eq_mul, ofScalars_norm_le, ofScalars_radius_eq_inv_of_tendsto, ofScalars_radius_eq_inv_of_tendsto_ENNReal, ofScalars_radius_eq_of_tendsto, ofScalars_radius_eq_top_of_tendsto, ofScalars_radius_eq_zero_of_tendsto, ofScalars_radius_ge_inv_of_tendsto, ofScalars_series_eq_iff, ofScalars_series_eq_zero, ofScalars_series_eq_zero_of_scalar_zero, ofScalars_series_injective, ofScalars_series_of_subsingleton, ofScalars_smul, ofScalars_sub, ofScalars_sum_eq	32
Total	35

FormalMultilinearSeries

Definitions

Name	Category	Theorems
ofScalars 📖	CompOp	50 math math: PeriodPair.hasFPowerSeriesAt_weierstrassPExcept, ofScalars_apply_eq', NormedSpace.expSeries_eq_ofScalars, ofScalars_eq_zero_of_scalar_zero, ofScalars_series_eq_zero_of_scalar_zero, ofScalars_radius_eq_inv_of_tendsto_ENNReal, Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, ofScalars_apply_eq, ofScalars_eq_zero, ofScalars_apply_zero, ofScalars_radius_eq_inv_of_tendsto, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, ofScalars_series_of_subsingleton, ofScalars_series_eq_iff, ofScalars_add, Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, ofScalars_sub, ofScalars_radius_eq_of_tendsto, Real.one_div_one_sub_hasFPowerSeriesOnBall_zero, coeff_ofScalars, Real.one_div_sub_hasFPowerSeriesOnBall_zero, ofScalars_norm_le, inv_le_ofScalars_radius_of_tendsto, Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero, Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, ProbabilityTheory.hasFPowerSeriesAt_mgf, Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero, formalMultilinearSeries_geometric_eq_ofScalars, AnalyticAt.hasFPowerSeriesAt, ofScalars_radius_eq_zero_of_tendsto, Real.hasFPowerSeriesOnBall_linear_zero, hasFPowerSeriesOnBall_cuspFunction, Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, ofScalars_smul, Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, ofScalars_comp_neg_id, ofScalars_series_eq_zero, ofScalars_comp_neg, Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero, ofScalars_series_injective, Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero, ofScalars_radius_eq_top_of_tendsto, Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, ofScalars_radius_ge_inv_of_tendsto, ofScalars_norm_eq_mul, Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero, Complex.one_div_sub_hasFPowerSeriesOnBall_zero, ofScalars_norm
ofScalarsSubmodule 📖	CompOp	—
ofScalarsSum 📖	CompOp	7 math math: ofScalarsSum_op, ofScalarsSum_of_subsingleton, ofScalarsSum_zero, ofScalarsSum_eq_tsum, ofScalars_sum_eq, ofScalarsSum_unop, NormedSpace.exp_eq_ofScalarsSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_ofScalars 📖	mathematical	—	coeff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace ofScalars 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	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing List.prod_ofFn Finset.prod_congr Finset.prod_const_one mul_one
inv_le_ofScalars_radius_of_tendsto 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.toReal	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal NNReal NNReal.instInv radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	—	ENNReal.le_of_forall_nnreal_lt NonUnitalSeminormedRing.toIsTopologicalRing ENNReal.instCanonicallyOrderedAdd le_radius_of_summable_norm Summable.of_norm_bounded_eventually Real.instCompleteSpace summable_of_ratio_test_tendsto_lt_one NNReal.lt_inv_iff_mul_lt ENNReal.coe_lt_coe Filter.Eventually.mp Filter.Tendsto.eventually_ne T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal NNReal.coe_ne_zero Filter.Eventually.of_forall norm_mul NormedDivisionRing.toNormMulClass norm_norm norm_pow NormedDivisionRing.to_normOneClass NNReal.abs_eq NormMulClass.toNoZeroDivisors isReduced_of_noZeroDivisors Real.instNontrivial Filter.mp_mem Filter.eventually_cofinite_ne Filter.univ_mem' NNReal.norm_eq mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing ofScalars_norm_le le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le NNReal.instCanonicallyOrderedAdd
ofScalarsSum_eq_tsum 📖	mathematical	—	ofScalarsSum tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	ofScalars_sum_eq
ofScalarsSum_of_subsingleton 📖	mathematical	—	ofScalarsSum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ofScalarsSum.congr_simp Subsingleton.eq_zero ofScalarsSum_zero smul_zero
ofScalarsSum_op 📖	mathematical	—	ofScalarsSum MulOpposite MulOpposite.instRing MulOpposite.instAlgebra Semifield.toCommSemiring Field.toSemifield Ring.toSemiring MulOpposite.instTopologicalSpaceMulOpposite instIsTopologicalRingMulOpposite NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulOpposite.op	—	instIsTopologicalRingMulOpposite ofScalars_sum_eq tsum_op
ofScalarsSum_unop 📖	mathematical	—	ofScalarsSum MulOpposite.unop MulOpposite MulOpposite.instRing MulOpposite.instAlgebra Semifield.toCommSemiring Field.toSemifield Ring.toSemiring MulOpposite.instTopologicalSpaceMulOpposite instIsTopologicalRingMulOpposite NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	instIsTopologicalRingMulOpposite ofScalars_sum_eq tsum_unop
ofScalarsSum_zero 📖	mathematical	—	ofScalarsSum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ofScalarsSum_eq_tsum ofScalars_apply_zero tsum_pi_single
ofScalars_add 📖	mathematical	—	ofScalars Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing FormalMultilinearSeries DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidFormalMultilinearSeries	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul Pi.add_def Module.add_smul smulCommClass_self
ofScalars_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 ofScalars Algebra.toSMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	List.ofFn_const List.prod_replicate
ofScalars_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 ofScalars Algebra.toSMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	List.ofFn_const List.prod_replicate
ofScalars_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 ofScalars MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.single Algebra.toSMul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ofScalars.eq_1 Pi.single_eq_same List.ofFn_const List.prod_replicate MulZeroClass.zero_mul smul_zero Pi.single_eq_of_ne
ofScalars_comp_neg 📖	mathematical	—	compContinuousLinearMap 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 ofScalars ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.neg DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup RingHomCompTriple.right_ids ContinuousLinearMap.id_comp ContinuousLinearMap.neg_comp RingHomCompTriple.ids compContinuousLinearMap_comp ofScalars_comp_neg_id
ofScalars_comp_neg_id 📖	mathematical	—	compContinuousLinearMap 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 ofScalars ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.neg DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup ContinuousLinearMap.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup ContinuousMultilinearMap.ext Nat.even_or_odd List.prod_map_neg Even.neg_one_pow one_mul Odd.neg_one_pow neg_mul smul_neg smulCommClass_self neg_smul
ofScalars_eq_zero 📖	mathematical	—	ofScalars ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	ofScalars.eq_1 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul smulCommClass_self smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain IsTopologicalRing.to_topologicalAddGroup GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Function.mt ContinuousMultilinearMap.ext_iff List.ofFn_const List.prod_replicate one_pow NeZero.one
ofScalars_eq_zero_of_scalar_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	ofScalars ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.instZero	—	ofScalars.eq_1 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul smulCommClass_self zero_smul
ofScalars_norm 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype ofScalars NonUnitalSeminormedRing.toIsTopologicalRing NormedField.toNorm	—	NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ofScalars_norm_eq_mul ContinuousMultilinearMap.norm_mkPiAlgebraFin mul_one
ofScalars_norm_eq_mul 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype ofScalars NonUnitalSeminormedRing.toIsTopologicalRing Real Real.instMul NormedField.toNorm CommSemiring.toSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ContinuousMultilinearMap.mkPiAlgebraFin IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring	—	NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ofScalars.eq_1 norm_smul NormedSpace.toNormSMulClass smulCommClass_self
ofScalars_norm_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype ofScalars NonUnitalSeminormedRing.toIsTopologicalRing NormedField.toNorm	—	NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ofScalars_norm_eq_mul mul_le_of_le_one_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos
ofScalars_radius_eq_inv_of_tendsto 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.toReal	radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing ENNReal.ofNNReal NNReal NNReal.instInv	—	le_antisymm NonUnitalSeminormedRing.toIsTopologicalRing ENNReal.le_of_forall_nnreal_lt ENNReal.coe_le_coe NNReal.le_inv_iff_mul_le summable_norm_mul_pow Mathlib.Tactic.Contrapose.contrapose₁ not_summable_of_ratio_test_tendsto_gt_one ofScalars_norm MulZeroClass.zero_mul NNReal.instCanonicallyOrderedAdd inv_le_ofScalars_radius_of_tendsto
ofScalars_radius_eq_inv_of_tendsto_ENNReal 📖	mathematical	Filter.Tendsto ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofReal Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace	radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing ENNReal.instInv	—	NonUnitalSeminormedRing.toIsTopologicalRing ENNReal.trichotomy ENNReal.inv_zero ofScalars_radius_eq_top_of_tendsto Filter.Tendsto.congr' Filter.mp_mem Filter.univ_mem' ofReal_norm ENNReal.toReal_div toReal_enorm Filter.Tendsto.comp ENNReal.tendsto_toReal ENNReal.zero_ne_top radius_eq_top_of_eventually_eq_zero instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.eventually_atTop Filter.Tendsto.eventually_ne T5Space.toT1Space ENNReal.instT5Space Nat.le_induction ofScalars_eq_zero_of_scalar_zero Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup ofScalars_series_of_subsingleton Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq LE.le.trans ENNReal.div_eq_top norm_zero ENNReal.ofReal_zero ENNReal.inv_top ofScalars_radius_eq_zero_of_tendsto Filter.tendsto_add_atTop_iff_nat ENNReal.tendsto_ofReal_nhds_top ENNReal.top_ne_zero ENNReal.ofReal_div_of_pos Ne.lt_of_le norm_nonneg ENNReal.toReal_ne_zero LT.lt.ne ENNReal.toNNReal_ne_zero ENNReal.coe_inv ENNReal.coe_toNNReal ofScalars_radius_eq_inv_of_tendsto
ofScalars_radius_eq_of_tendsto 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.toReal	radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing ENNReal.ofNNReal	—	inv_div Filter.Tendsto.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal NNReal.coe_ne_zero NonUnitalSeminormedRing.toIsTopologicalRing inv_inv ofScalars_radius_eq_inv_of_tendsto inv_ne_zero
ofScalars_radius_eq_top_of_tendsto 📖	mathematical	Filter.Eventually MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing Top.top ENNReal instTopENNReal	—	radius_eq_top_of_summable_norm NonUnitalSeminormedRing.toIsTopologicalRing Summable.comp_nat_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal zero_pow MulZeroClass.mul_zero Summable.of_norm_bounded_eventually Real.instCompleteSpace summable_of_ratio_test_tendsto_lt_one zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Filter.Eventually.mp Filter.Eventually.of_forall norm_mul NormedDivisionRing.toNormMulClass norm_norm norm_pow NormedDivisionRing.to_normOneClass NNReal.abs_eq NormMulClass.toNoZeroDivisors isReduced_of_noZeroDivisors Real.instNontrivial NNReal.coe_zero Filter.mp_mem Filter.eventually_cofinite_ne Filter.univ_mem' NNReal.norm_eq mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing ofScalars_norm_le le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le NNReal.instCanonicallyOrderedAdd
ofScalars_radius_eq_zero_of_tendsto 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder Real.instPreorder	radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing ENNReal instZeroENNReal	—	NonUnitalSeminormedRing.toIsTopologicalRing ENNReal.le_of_forall_nnreal_lt ENNReal.coe_zero ENNReal.coe_le_coe summable_norm_mul_pow Mathlib.Tactic.Contrapose.contrapose₁ not_summable_of_ratio_norm_eventually_ge Nat.instAtLeastTwoHAddOfNat IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.congr' Filter.mp_mem Filter.univ_mem' mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass norm_norm norm_mul ofScalars_norm norm_zero div_zero norm_pow NormedDivisionRing.to_normOneClass NNReal.abs_eq isReduced_of_noZeroDivisors tendsto_const_nhds Filter.eventually_ne_atTop Nat.instNoMaxOrder Filter.Tendsto.eventually_ge_atTop NNReal.norm_eq mul_comm mul_assoc div_le_div_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Ne.lt_of_le norm_nonneg mul_div_assoc pow_succ div_mul_cancel_left₀ NNReal.coe_inv ENNReal.instCanonicallyOrderedAdd
ofScalars_radius_ge_inv_of_tendsto 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.toReal	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal NNReal NNReal.instInv radius NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing ofScalars NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing	—	inv_le_ofScalars_radius_of_tendsto
ofScalars_series_eq_iff 📖	mathematical	—	ofScalars	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ofScalars_series_injective
ofScalars_series_eq_zero 📖	mathematical	—	ofScalars FormalMultilinearSeries 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup
ofScalars_series_eq_zero_of_scalar_zero 📖	mathematical	—	ofScalars Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing FormalMultilinearSeries DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup ofScalars_eq_zero_of_scalar_zero
ofScalars_series_injective 📖	mathematical	—	FormalMultilinearSeries 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 ofScalars	—	Function.mtr IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul Mathlib.Tactic.Push.not_forall_eq Function.ne_iff List.ofFn_const List.prod_replicate one_pow smul_left_injective IsDomain.toIsCancelMulZero Field.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors one_ne_zero NeZero.one
ofScalars_series_of_subsingleton 📖	mathematical	—	ofScalars FormalMultilinearSeries 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup
ofScalars_smul 📖	mathematical	—	ofScalars Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id FormalMultilinearSeries DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup instAddCommMonoidFormalMultilinearSeries instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid CommRing.toRing	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup smulCommClass_self Pi.smul_def smul_smul
ofScalars_sub 📖	mathematical	—	ofScalars Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing FormalMultilinearSeries 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 AddCommGroup.toAddGroup instAddCommGroup Ring.toAddCommGroup IsTopologicalRing.to_topologicalAddGroup	—	ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup ContinuousMultilinearMap.ext smulCommClass_self sub_smul
ofScalars_sum_eq 📖	mathematical	—	ofScalarsSum tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	tsum_congr ofScalars_apply_eq

---

← Back to Index