Evaluation

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

Statistics

Metric	Count
Definitions HasEval, aeval, eval₂, eval₂Hom, hasEvalIdeal	5
Theorems toMvPowerSeries_isDenseInducing, toMvPowerSeries_isUniformInducing, toMvPowerSeries_uniformContinuous, X, add, hpow, map, mono, mul_left, mul_right, pow, tendsto_zero, zero, aeval_coe, aeval_eq_sum, aeval_unique, coe_aeval, coe_eval₂Hom, coe_hasEvalIdeal, comp_aeval, comp_eval₂, continuous_aeval, continuous_eval₂, eval₂Hom_eq_extend, eval₂_C, eval₂_X, eval₂_coe, eval₂_eq_tsum, eval₂_unique, hasEval_def, hasSum_aeval, hasSum_eval₂, mem_hasEvalIdeal_iff, uniformContinuous_eval₂	34
Total	39

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMvPowerSeries_isDenseInducing 📖	mathematical	—	IsDenseInducing MvPolynomial CommRing.toCommSemiring MvPowerSeries UniformSpace.toTopologicalSpace MvPowerSeries.WithPiTopology.instTopologicalSpace toMvPowerSeries	—	IsUniformInducing.isDenseInducing toMvPowerSeries_isUniformInducing MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries
toMvPowerSeries_isUniformInducing 📖	mathematical	—	IsUniformInducing MvPolynomial CommRing.toCommSemiring MvPowerSeries MvPowerSeries.WithPiTopology.instUniformSpace toMvPowerSeries	—	isUniformInducing_iff
toMvPowerSeries_uniformContinuous 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.HasEval	UniformContinuous MvPolynomial commSemiring eval₂Hom	—	uniformContinuous_of_continuousAt_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass ContinuousAt.eq_1 map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Filter.HasBasis.tendsto_right_iff IsLinearTopology.hasBasis_ideal Filter.Eventually.exists_forall_of_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually_mem MvPowerSeries.HasEval.hpow Filter.mp_mem MvPowerSeries.HasEval.tendsto_zero Filter.univ_mem' zero_add pow_one Set.Nonempty.ne_empty Set.finite_Iic Nat.instCanonicallyOrderedAdd Continuous.tendsto' Continuous.comp MvPowerSeries.WithPiTopology.continuous_coeff continuous_induced_dom Set.Finite.eventually_all coe_eval₂Hom SetLike.mem_coe eval₂_eq Ideal.sum_mem Ideal.mul_mem_right Ideal.instIsTwoSided_1 Ideal.mul_mem_left Mathlib.Tactic.Push.not_forall_eq Ideal.prod_mem Ideal.pow_mem_of_pow_mem Nat.sInf_mem

MvPowerSeries

Definitions

Name	Category	Theorems
HasEval 📖	CompData	9 math math: mem_hasEvalIdeal_iff, HasEval.zero, hasSubst_iff_hasEval_of_discreteTopology, hasEval_def, coe_hasEvalIdeal, HasEval.X, PowerSeries.hasEval_iff, HasSubst.hasEval, PowerSeries.hasEval
aeval 📖	CompOp	11 math math: continuous_aeval, substAlgHom_eq_aeval, hasSum_aeval, comp_aeval, aeval_coe, comp_subst_apply, coe_aeval, aeval_eq_sum, comp_subst, comp_substAlgHom, aeval_unique
eval₂ 📖	CompOp	13 math math: eval₂_coe, subst_eq_eval₂, eval₂_X, continuous_eval₂, coe_eval₂Hom, eval₂_subst, eval₂_eq_tsum, coe_aeval, eval₂_unique, uniformContinuous_eval₂, eval₂_C, hasSum_eval₂, comp_eval₂
eval₂Hom 📖	CompOp	2 math math: eval₂Hom_eq_extend, coe_eval₂Hom
hasEvalIdeal 📖	CompOp	2 math math: mem_hasEvalIdeal_iff, coe_hasEvalIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_coe 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike aeval MvPolynomial.toMvPowerSeries MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra MvPolynomial.aeval	—	coe_aeval MvPolynomial.aeval_def eval₂_coe
aeval_eq_sum 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike aeval tsum Finsupp MulZeroClass.toZero Nat.instMulZeroClass 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 Finsupp.prod CommRing.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional hasSum_aeval
aeval_unique 📖	mathematical	Continuous MvPowerSeries 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	—	DFunLike.ext' HasEval.map HasEval.X coe_aeval eval₂_unique continuous_algebraMap MvPolynomial.aeval_X_left_apply MvPolynomial.comp_aeval_apply MvPolynomial.aeval_def MvPolynomial.coe_X
coe_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike aeval eval₂ algebraMap	—	coe_eval₂Hom
coe_eval₂Hom 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	MvPowerSeries instSemiring eval₂Hom eval₂	—	MvPolynomial.toMvPowerSeries_isDenseInducing Classical.choose_eq IsDenseInducing.extend_eq UniformContinuous.continuous MvPolynomial.toMvPowerSeries_uniformContinuous eval₂Hom_eq_extend
coe_hasEvalIdeal 📖	mathematical	—	SetLike.coe Submodule Pi.semiring 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 MvPowerSeries instSemiring instAlgebra Algebra.id aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike AlgHom.toRingHom HasEval.map	—	DFunLike.ext' HasEval.map coe_aeval AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe comp_eval₂ continuous_algebraMap AlgHom.comp_algebraMap_of_tower IsScalarTower.left
comp_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	MvPowerSeries eval₂ RingHom.comp	—	eval₂_unique Continuous.comp HasEval.map continuous_eval₂ eval₂_coe MvPolynomial.coe_eval₂Hom RingHom.comp_apply MvPolynomial.comp_eval₂Hom
continuous_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	Continuous MvPowerSeries WithPiTopology.instTopologicalSpace DFunLike.coe AlgHom CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike aeval	—	coe_aeval continuous_eval₂ continuous_algebraMap
continuous_eval₂ 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	MvPowerSeries WithPiTopology.instTopologicalSpace eval₂	—	UniformContinuous.continuous uniformContinuous_eval₂
eval₂Hom_eq_extend 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	MvPowerSeries instSemiring eval₂Hom IsDenseInducing.extend MvPolynomial WithPiTopology.instTopologicalSpace MvPolynomial.toMvPowerSeries MvPolynomial.toMvPowerSeries_isDenseInducing MvPolynomial.eval₂	—	—
eval₂_C 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instSemiring RingHom.instFunLike C	—	MvPolynomial.coe_C eval₂_coe MvPolynomial.eval₂_C
eval₂_X 📖	mathematical	—	eval₂ X CommSemiring.toSemiring CommRing.toCommSemiring	—	MvPolynomial.coe_X eval₂_coe MvPolynomial.eval₂_X
eval₂_coe 📖	mathematical	—	eval₂ MvPolynomial.toMvPowerSeries CommRing.toCommSemiring MvPolynomial.eval₂	—	MvPolynomial.toMvPowerSeries_isDenseInducing eval₂.eq_1
eval₂_eq_tsum 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike HasEval	eval₂ tsum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap RingHom.id MvPowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Finsupp.prod CommRing.toCommMonoid 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 MvPowerSeries WithPiTopology.instTopologicalSpace MvPolynomial.toMvPowerSeries MvPolynomial.eval₂	eval₂	—	coe_eval₂Hom MvPolynomial.toMvPowerSeries_isDenseInducing IsDenseInducing.extend_unique
hasEval_def 📖	mathematical	—	HasEval IsTopologicallyNilpotent Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Filter.Tendsto Filter.cofinite nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
hasSum_aeval 📖	mathematical	HasEval UniformSpace.toTopologicalSpace	HasSum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Finsupp.prod CommRing.toCommMonoid 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 Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap RingHom.id MvPowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Finsupp.prod CommRing.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero eval₂ SummationFilter.unconditional	—	coe_eval₂Hom MvPolynomial.toMvPowerSeries_isDenseInducing eval₂Hom_eq_extend eval₂_coe MvPolynomial.eval₂_monomial HasSum.map WithPiTopology.hasSum_of_monomials_self RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass continuous_eval₂
mem_hasEvalIdeal_iff 📖	mathematical	—	Ideal Pi.semiring 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 MvPowerSeries WithPiTopology.instUniformSpace eval₂	—	coe_eval₂Hom uniformContinuous_uniformly_extend MvPolynomial.toMvPowerSeries_isUniformInducing WithPiTopology.denseRange_toMvPowerSeries MvPolynomial.toMvPowerSeries_uniformContinuous

MvPowerSeries.HasEval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X 📖	mathematical	—	MvPowerSeries.HasEval MvPowerSeries MvPowerSeries.instCommRing MvPowerSeries.WithPiTopology.instTopologicalSpace MvPowerSeries.X CommSemiring.toSemiring CommRing.toCommSemiring	—	MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero MvPowerSeries.constantCoeff_X MvPowerSeries.WithPiTopology.variables_tendsto_zero
add 📖	mathematical	MvPowerSeries.HasEval	Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicallyNilpotent.add hpow add_zero Filter.Tendsto.add tendsto_zero
hpow 📖	mathematical	MvPowerSeries.HasEval	IsTopologicallyNilpotent Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
map 📖	—	Continuous DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.HasEval	—	—	IsTopologicallyNilpotent.map RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass hpow Filter.Tendsto.comp Continuous.tendsto map_zero MonoidWithZeroHomClass.toZeroHomClass tendsto_zero
mono 📖	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder MvPowerSeries.HasEval	—	—	Filter.Tendsto.mono_right hpow nhds_mono tendsto_zero
mul_left 📖	mathematical	MvPowerSeries.HasEval	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicallyNilpotent.mul_left hpow IsLinearTopology.tendsto_mul_zero_of_right tendsto_zero
mul_right 📖	mathematical	MvPowerSeries.HasEval	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mul_left mul_comm
pow 📖	mathematical	MvPowerSeries.HasEval	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	MvPowerSeries.mem_hasEvalIdeal_iff Ideal.pow_mem_of_mem
tendsto_zero 📖	mathematical	MvPowerSeries.HasEval	Filter.Tendsto Filter.cofinite nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
zero 📖	mathematical	—	MvPowerSeries.HasEval Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicallyNilpotent.zero tendsto_const_nhds

---

← Back to Index