Evaluation

📁 Source: Mathlib/RingTheory/PowerSeries/Evaluation.lean

Statistics

Metric	Count
Definitions HasEval, aeval, eval₂, eval₂Hom, hasEvalIdeal	5
Theorems X, add, map, mono, mul_left, mul_right, zero, aeval_coe, aeval_eq_sum, aeval_unique, coe_aeval, coe_eval₂Hom, coe_hasEvalIdeal, comp_aeval, comp_eval₂, continuous_aeval, continuous_eval₂, eval₂_C, eval₂_X, eval₂_coe, eval₂_eq_tsum, eval₂_unique, hasEval, hasEval_def, hasEval_iff, hasSum_aeval, hasSum_eval₂, mem_hasEvalIdeal_iff, uniformContinuous_eval₂	29
Total	34

PowerSeries

Definitions

Name	Category	Theorems
HasEval 📖	MathDef	13 math math: HasEval.mul_left, HasEval.zero, coe_hasEvalIdeal, HasEval.add, HasSubst.hasEval, HasEval.mono, HasEval.mul_right, hasEval_iff, mem_hasEvalIdeal_iff, hasEval_def, HasEval.map, hasSubst_iff_hasEval_of_discreteTopology, HasEval.X
aeval 📖	CompOp	8 math math: hasSum_aeval, aeval_eq_sum, aeval_unique, comp_aeval, continuous_aeval, coe_aeval, substAlgHom_eq_aeval, aeval_coe
eval₂ 📖	CompOp	11 math math: eval₂_coe, eval₂_X, eval₂_eq_tsum, eval₂_C, coe_eval₂Hom, continuous_eval₂, coe_aeval, comp_eval₂, uniformContinuous_eval₂, eval₂_unique, hasSum_eval₂
eval₂Hom 📖	CompOp	1 math math: coe_eval₂Hom
hasEvalIdeal 📖	CompOp	2 math math: coe_hasEvalIdeal, mem_hasEvalIdeal_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_coe 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike aeval Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.aeval	—	coe_aeval Polynomial.aeval_def eval₂_coe
aeval_eq_sum 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike aeval tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing UniformSpace.toTopologicalSpace Algebra.toSMul LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries.instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional hasSum_aeval
aeval_unique 📖	mathematical	Continuous PowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe AlgHom CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike	aeval DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MvPowerSeries.instCommRing RingHom.instFunLike AlgHom.toRingHom MvPowerSeries.instSemiring MvPowerSeries.instAlgebra Algebra.id X HasEval.map WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace HasEval.X	—	MvPowerSeries.aeval_unique
coe_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike aeval eval₂ algebraMap	—	MvPowerSeries.coe_aeval hasEval
coe_eval₂Hom 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike eval₂Hom eval₂	—	MvPowerSeries.coe_eval₂Hom hasEval
coe_hasEvalIdeal 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike hasEvalIdeal setOf HasEval	—	—
comp_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace Continuous DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	AlgHom.comp PowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id aeval DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike AlgHom.toRingHom HasEval.map UniformSpace.toTopologicalSpace	—	MvPowerSeries.comp_aeval hasEval
comp_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	PowerSeries DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike eval₂ RingHom.comp	—	eval₂_unique Continuous.comp HasEval.map continuous_eval₂ eval₂_coe Polynomial.hom_eval₂
continuous_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	Continuous PowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe AlgHom CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike aeval	—	MvPowerSeries.continuous_aeval hasEval
continuous_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	Continuous PowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace eval₂	—	UniformContinuous.continuous uniformContinuous_eval₂
eval₂_C 📖	mathematical	—	eval₂ DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MvPowerSeries.instSemiring RingHom.instFunLike C	—	Polynomial.coe_C eval₂_coe Polynomial.eval₂_C
eval₂_X 📖	mathematical	—	eval₂ X CommSemiring.toSemiring CommRing.toCommSemiring	—	Polynomial.coe_X eval₂_coe Polynomial.eval₂_X
eval₂_coe 📖	mathematical	—	eval₂ Polynomial.toPowerSeries CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.eval₂	—	MvPolynomial.eval₂_const_pUnitAlgEquiv MvPolynomial.toMvPowerSeries_pUnitAlgEquiv MvPowerSeries.eval₂_coe
eval₂_eq_tsum 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	eval₂ tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing UniformSpace.toTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional hasSum_eval₂
eval₂_unique 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval PowerSeries WithPiTopology.instTopologicalSpace Polynomial.toPowerSeries Polynomial.eval₂	eval₂	—	MvPowerSeries.eval₂_unique hasEval MvPolynomial.toMvPowerSeries_pUnitAlgEquiv MvPolynomial.eval₂_pUnitAlgEquiv
hasEval 📖	mathematical	HasEval	MvPowerSeries.HasEval	—	hasEval_iff
hasEval_def 📖	mathematical	—	HasEval IsTopologicallyNilpotent Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
hasEval_iff 📖	mathematical	—	HasEval MvPowerSeries.HasEval	—	Filter.cofinite_eq_bot Finite.of_fintype MvPowerSeries.HasEval.hpow
hasSum_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing UniformSpace.toTopologicalSpace Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries MvPowerSeries.instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom MvPowerSeries.instSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike aeval SummationFilter.unconditional	—	coe_aeval algebraMap_smul IsScalarTower.right hasSum_eval₂ continuous_algebraMap
hasSum_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing UniformSpace.toTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero eval₂ SummationFilter.unconditional	—	MvPowerSeries.hasSum_eval₂ hasEval Finsupp.prod_pow Finset.prod_congr Finset.univ_unique Finset.prod_singleton Finsupp.single_eq_same Function.Injective.hasSum_iff Finsupp.single_injective Finsupp.unique_ext
mem_hasEvalIdeal_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule hasEvalIdeal HasEval	—	HasEval.zero HasEval.mul_left
uniformContinuous_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	UniformContinuous PowerSeries WithPiTopology.instUniformSpace eval₂	—	MvPowerSeries.uniformContinuous_eval₂ hasEval

PowerSeries.HasEval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X 📖	mathematical	—	PowerSeries.HasEval PowerSeries MvPowerSeries.instCommRing PowerSeries.WithPiTopology.instTopologicalSpace PowerSeries.X CommSemiring.toSemiring CommRing.toCommSemiring	—	PowerSeries.hasEval_iff MvPowerSeries.HasEval.X
add 📖	mathematical	PowerSeries.HasEval	PowerSeries.HasEval Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPowerSeries.HasEval.add
map 📖	mathematical	Continuous DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike PowerSeries.HasEval	PowerSeries.HasEval DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	MvPowerSeries.HasEval.map
mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder PowerSeries.HasEval	PowerSeries.HasEval	—	MvPowerSeries.HasEval.mono
mul_left 📖	mathematical	PowerSeries.HasEval	PowerSeries.HasEval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPowerSeries.HasEval.mul_left
mul_right 📖	mathematical	PowerSeries.HasEval	PowerSeries.HasEval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPowerSeries.HasEval.mul_right
zero 📖	mathematical	—	PowerSeries.HasEval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	PowerSeries.hasEval_iff MvPowerSeries.HasEval.zero

---

← Back to Index