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	8 math math: HasEval.zero, coe_hasEvalIdeal, HasSubst.hasEval, hasEval_iff, mem_hasEvalIdeal_iff, hasEval_def, 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 instSemiring CommSemiring.toSemiring 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 instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike aeval tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow 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 instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike	aeval RingHom Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike AlgHom.toRingHom X HasEval.map HasEval.X	—	MvPowerSeries.aeval_unique
coe_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring 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	PowerSeries instSemiring 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 instSemiring instAlgebra Algebra.id aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike AlgHom.toRingHom HasEval.map	—	MvPowerSeries.comp_aeval hasEval
comp_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	PowerSeries 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 DFunLike.coe AlgHom CommRing.toCommSemiring instSemiring CommSemiring.toSemiring 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	PowerSeries WithPiTopology.instTopologicalSpace eval₂	—	UniformContinuous.continuous uniformContinuous_eval₂
eval₂_C 📖	mathematical	—	eval₂ DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring 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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap RingHom.id PowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow 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 Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom instSemiring 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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap RingHom.id PowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow 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 PowerSeries.instCommRing PowerSeries.WithPiTopology.instTopologicalSpace PowerSeries.X CommSemiring.toSemiring CommRing.toCommSemiring	—	PowerSeries.hasEval_iff MvPowerSeries.HasEval.X
add 📖	mathematical	PowerSeries.HasEval	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPowerSeries.HasEval.add
map 📖	—	Continuous DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike PowerSeries.HasEval	—	—	MvPowerSeries.HasEval.map
mono 📖	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder PowerSeries.HasEval	—	—	MvPowerSeries.HasEval.mono
mul_left 📖	mathematical	PowerSeries.HasEval	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPowerSeries.HasEval.mul_left
mul_right 📖	mathematical	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