Substitution

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

Statistics

Metric	Count
Definitions HasSubst, ideal, subst, substAlgHom	4
Theorems rescaleUnit, toPowerSeries_toMvPowerSeries, X, X', X_pow, add, comp, const, eventually_coeff_pow_eq_zero, hasEval, monomial, monomial', mul_left, mul_right, of_constantCoeff_zero, of_constantCoeff_zero', smul, smul', smul_X, smul_X', zero, zero', coe_substAlgHom, coeff_subst, coeff_subst', coeff_subst_finite, coeff_subst_finite', constantCoeff_subst, constantCoeff_subst_eq_zero, hasSubst_iff, hasSubst_iff_hasEval_of_discreteTopology, le_order_subst, le_order_subst_left, le_order_subst_left', le_order_subst_right, le_order_subst_right', le_weightedOrder_subst, map_algebraMap_eq_subst_X, map_subst, substAlgHom_X, substAlgHom_coe, substAlgHom_comp_substAlgHom, substAlgHom_comp_substAlgHom_apply, substAlgHom_eq_aeval, subst_X, subst_add, subst_coe, subst_comp_subst, subst_comp_subst_apply, subst_mul, subst_pow, subst_smul	52
Total	56

MvPowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rescaleUnit 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike rescale PowerSeries PowerSeries.instSemiring PowerSeries.rescale	—	PowerSeries.ext PowerSeries.coeff_rescale PowerSeries.coeff.eq_1 coeff_rescale Finsupp.prod_single_index pow_zero

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPowerSeries_toMvPowerSeries 📖	mathematical	—	toPowerSeries CommSemiring.toSemiring CommRing.toCommSemiring MvPolynomial.toMvPowerSeries DFunLike.coe AlgHom Polynomial MvPolynomial semiring MvPolynomial.commSemiring algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgHom.funLike aeval MvPolynomial.X	—	AlgHom.comp_apply AlgHom.congr_fun algHom_ext coe_X aeval_X MvPolynomial.coe_X

PowerSeries

Definitions

Name	Category	Theorems
HasSubst 📖	MathDef	13 math math: HasSubst.zero, HasSubst.X', HasSubst.X_pow, HasSubst.of_constantCoeff_zero', HasSubst.smul_X', HasSubst.zero', HasSubst.X, HasSubst.monomial', hasSubst_iff, HasSubst.of_constantCoeff_zero, HasSubst.monomial, HasSubst.smul_X, hasSubst_iff_hasEval_of_discreteTopology
subst 📖	CompOp	24 math math: constantCoeff_subst, le_order_subst_left', expand_subst, expand_apply, subst_mul, coeff_subst, subst_pow, le_order_subst_right', constantCoeff_subst_eq_zero, map_subst, map_algebraMap_eq_subst_X, subst_coe, subst_add, le_order_subst, subst_comp_subst_apply, subst_X, coeff_subst', derivative_subst, le_order_subst_right, subst_smul, coe_substAlgHom, le_weightedOrder_subst, le_order_subst_left, subst_comp_subst
substAlgHom 📖	CompOp	7 math math: substAlgHom_X, substAlgHom_comp_substAlgHom, HasSubst.comp, substAlgHom_eq_aeval, substAlgHom_coe, substAlgHom_comp_substAlgHom_apply, coe_substAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_substAlgHom 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring instAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.funLike substAlgHom subst	—	MvPowerSeries.coe_substAlgHom HasSubst.const
coeff_subst 📖	mathematical	HasSubst	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike MvPowerSeries.coeff subst finsum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul PowerSeries instAddCommMonoid instModule coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring	—	subst.eq_1 MvPowerSeries.coeff_subst HasSubst.const RingHomInvPair.ids finsum_comp_equiv finsum_congr Finsupp.LinearEquiv.finsuppUnique_symm_apply Finsupp.prod_single_index pow_zero
coeff_subst' 📖	mathematical	HasSubst	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff subst finsum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	coeff_subst
coeff_subst_finite 📖	mathematical	HasSubst	Set.Finite Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff MvPowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule MvPowerSeries.coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring	—	RingHomInvPair.ids Equiv.preimage_eq_iff_eq_image Function.support_comp_eq_preimage Equiv.eq_comp_symm Finsupp.prod_pow Finset.prod_congr Finset.univ_unique Finset.prod_singleton Finsupp.LinearEquiv.finsuppUnique_symm_apply Finsupp.single_eq_same Set.Finite.image MvPowerSeries.coeff_subst_finite HasSubst.const
coeff_subst_finite' 📖	mathematical	HasSubst	Set.Finite Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	coeff_subst_finite
constantCoeff_subst 📖	mathematical	HasSubst	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.constantCoeff subst finsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul LinearMap RingHom.id PowerSeries instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	coeff_subst
constantCoeff_subst_eq_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing PowerSeries instSemiring constantCoeff	subst	—	constantCoeff_subst HasSubst.of_constantCoeff_zero finsum_eq_zero_of_forall_eq_zero coeff_zero_eq_constantCoeff pow_zero zero_smul map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_pow smul_zero
hasSubst_iff 📖	mathematical	—	HasSubst MvPowerSeries.HasSubst MvPowerSeries	—	MvPowerSeries.hasSubst_of_constantCoeff_nilpotent Finite.of_fintype MvPowerSeries.HasSubst.const_coeff
hasSubst_iff_hasEval_of_discreteTopology 📖	mathematical	—	HasSubst HasEval MvPowerSeries MvPowerSeries.instCommRing MvPowerSeries.WithPiTopology.instTopologicalSpace	—	hasSubst_iff MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology hasEval_iff Function.const_def
le_order_subst 📖	mathematical	HasSubst	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat MvPowerSeries.order CommRing.toCommSemiring order subst	—	LE.le.trans order_eq_order ciInf_unique MvPowerSeries.le_order_subst hasSubst_iff
le_order_subst_left 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat order MvPowerSeries.order subst Algebra.id	—	LE.le.trans ENat.self_le_mul_left MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero le_order_subst HasSubst.of_constantCoeff_zero
le_order_subst_left' 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat order subst Algebra.id	—	order_eq_order le_order_subst_left
le_order_subst_right 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing PowerSeries instSemiring constantCoeff	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat MvPowerSeries.order subst Algebra.id	—	LE.le.trans ENat.self_le_mul_right order_ne_zero_iff_constCoeff_eq_zero le_order_subst HasSubst.of_constantCoeff_zero
le_order_subst_right' 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat order subst Algebra.id	—	order_eq_order le_order_subst_right
le_weightedOrder_subst 📖	mathematical	HasSubst	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat order CommRing.toCommSemiring MvPowerSeries.weightedOrder subst	—	LE.le.trans iInf_congr_Prop mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono order_le Finsupp.unique_ext Finsupp.single_eq_same nsmul_eq_mul Finsupp.sum_fintype CharP.cast_eq_zero CharP.ofCharZero MulZeroClass.zero_mul Finset.sum_congr Finset.univ_unique Finset.sum_singleton MvPowerSeries.le_weightedOrder_subst hasSubst_iff
map_algebraMap_eq_subst_X 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike map algebraMap subst X	—	MvPowerSeries.map_algebraMap_eq_subst_X
map_subst 📖	mathematical	HasSubst	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.map subst Algebra.id PowerSeries instSemiring map	—	MvPowerSeries.ext MvPowerSeries.coeff_map coeff_subst IsNilpotent.map RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AddMonoidHom.map_finsum coeff_subst_finite finsum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MonoidWithZeroHomClass.toMonoidHomClass
substAlgHom_X 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring instAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.funLike substAlgHom X	—	Polynomial.coe_X substAlgHom_coe Polynomial.aeval_X
substAlgHom_coe 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring instAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.funLike substAlgHom Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.aeval	—	Polynomial.toPowerSeries_toMvPowerSeries HasSubst.const substAlgHom.eq_1 MvPowerSeries.coe_substAlgHom MvPowerSeries.subst_coe AlgHom.comp_apply AlgHom.congr_fun Polynomial.algHom_ext Polynomial.aeval_X MvPolynomial.aeval_X
substAlgHom_comp_substAlgHom 📖	mathematical	HasSubst	AlgHom.comp PowerSeries MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring instAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.restrictScalars instIsScalarTower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.toSMul IsScalarTower.right MvPowerSeries.instIsScalarTower NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing substAlgHom DFunLike.coe AlgHom AlgHom.funLike HasSubst.comp	—	MvPowerSeries.substAlgHom_comp_substAlgHom HasSubst.const
substAlgHom_comp_substAlgHom_apply 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring instAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.funLike substAlgHom HasSubst.comp	—	DFunLike.congr_fun instIsScalarTower IsScalarTower.right MvPowerSeries.instIsScalarTower HasSubst.comp substAlgHom_comp_substAlgHom
substAlgHom_eq_aeval 📖	mathematical	HasSubst	substAlgHom aeval MvPowerSeries MvPowerSeries.instCommRing MvPowerSeries.WithPiTopology.instUniformSpace instIsUniformAddGroupOfDiscreteUniformity AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology MvPowerSeries.WithPiTopology.instIsUniformAddGroup AddCommGroup.toAddGroup Ring.toAddCommGroup MvPowerSeries.WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace MvPowerSeries.WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace MvPowerSeries.WithPiTopology.instIsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology Semiring.toModule Ring.toSemiring MulOpposite MulOpposite.instRing Semiring.toOppositeModule MvPowerSeries.instAlgebra CommRing.toCommSemiring CommSemiring.toSemiring MvPowerSeries.WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval	—	AlgHom.ext instIsUniformAddGroupOfDiscreteUniformity IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology MvPowerSeries.WithPiTopology.instIsUniformAddGroup MvPowerSeries.WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace MvPowerSeries.WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace MvPowerSeries.WithPiTopology.instIsTopologicalRing MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology MvPowerSeries.WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval MvPowerSeries.substAlgHom_apply HasSubst.const MvPowerSeries.HasSubst.hasEval MvPowerSeries.substAlgHom_eq_aeval
subst_X 📖	mathematical	HasSubst	subst X CommSemiring.toSemiring CommRing.toCommSemiring	—	coe_substAlgHom substAlgHom_X
subst_add 📖	mathematical	HasSubst	subst PowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing MvPowerSeries MvPowerSeries.instCommRing	—	coe_substAlgHom map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
subst_coe 📖	mathematical	HasSubst	subst Polynomial.toPowerSeries CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial MvPowerSeries Polynomial.semiring MvPowerSeries.instSemiring Polynomial.algebraOfAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.funLike Polynomial.aeval	—	coe_substAlgHom substAlgHom_coe
subst_comp_subst 📖	mathematical	HasSubst	PowerSeries MvPowerSeries subst	—	instIsScalarTower IsScalarTower.right MvPowerSeries.instIsScalarTower HasSubst.comp coe_substAlgHom substAlgHom.congr_simp substAlgHom_comp_substAlgHom
subst_comp_subst_apply 📖	mathematical	HasSubst	subst	—	subst_comp_subst
subst_mul 📖	mathematical	HasSubst	subst PowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring MvPowerSeries	—	coe_substAlgHom map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
subst_pow 📖	mathematical	HasSubst	subst PowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring MvPowerSeries MvPowerSeries.instSemiring	—	coe_substAlgHom map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
subst_smul 📖	mathematical	HasSubst	subst PowerSeries Algebra.toSMul CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra MvPowerSeries MvPowerSeries.instSemiring MvPowerSeries.instAlgebra	—	coe_substAlgHom AlgHom.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul instIsScalarTower IsScalarTower.right MvPowerSeries.instIsScalarTower

PowerSeries.HasSubst

Definitions

Name	Category	Theorems
ideal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X 📖	mathematical	—	PowerSeries.HasSubst MvPowerSeries.X CommSemiring.toSemiring CommRing.toCommSemiring	—	MvPowerSeries.constantCoeff_X
X' 📖	mathematical	—	PowerSeries.HasSubst PowerSeries.X CommSemiring.toSemiring CommRing.toCommSemiring	—	X
X_pow 📖	mathematical	—	PowerSeries.HasSubst PowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring PowerSeries.X	—	of_constantCoeff_zero' map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass PowerSeries.constantCoeff_X zero_pow
add 📖	mathematical	PowerSeries.HasSubst	MvPowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPowerSeries.instCommRing	—	Commute.isNilpotent_add Commute.all
comp 📖	mathematical	PowerSeries.HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring PowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring PowerSeries.instAlgebra Algebra.id MvPowerSeries.instAlgebra AlgHom.funLike PowerSeries.substAlgHom	—	MvPowerSeries.IsNilpotent_subst const
const 📖	mathematical	PowerSeries.HasSubst	MvPowerSeries.HasSubst	—	PowerSeries.hasSubst_iff
eventually_coeff_pow_eq_zero 📖	mathematical	PowerSeries.HasSubst	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_of_mem Filter.Ici_mem_atTop PowerSeries.coeff_of_lt_order le_iff_exists_add Nat.instCanonicallyOrderedAdd Set.mem_Ici pow_add lt_imp_lt_of_le_of_le le_refl PowerSeries.order_mul_ge pow_mul add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid PowerSeries.le_order_pow_of_constantCoeff_eq_zero map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_add_right le_rfl Nat.cast_lt IsOrderedRing.toZeroLEOneClass
hasEval 📖	mathematical	PowerSeries.HasSubst	PowerSeries.HasEval MvPowerSeries MvPowerSeries.instCommRing MvPowerSeries.WithPiTopology.instTopologicalSpace	—	MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
monomial 📖	mathematical	—	PowerSeries.HasSubst DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instAddCommMonoid Semiring.toModule MvPowerSeries.instModule LinearMap.instFunLike MvPowerSeries.monomial	—	of_constantCoeff_zero MvPowerSeries.coeff_zero_eq_constantCoeff MvPowerSeries.coeff_monomial
monomial' 📖	mathematical	—	PowerSeries.HasSubst DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instAddCommMonoid Semiring.toModule PowerSeries.instModule LinearMap.instFunLike PowerSeries.monomial	—	monomial Finsupp.single_ne_zero
mul_left 📖	mathematical	PowerSeries.HasSubst	MvPowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Commute.isNilpotent_mul_right Commute.all
mul_right 📖	mathematical	PowerSeries.HasSubst	MvPowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Commute.isNilpotent_mul_left Commute.all
of_constantCoeff_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	PowerSeries.HasSubst	—	—
of_constantCoeff_zero' 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring PowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	PowerSeries.HasSubst	—	of_constantCoeff_zero
smul 📖	mathematical	PowerSeries.HasSubst	MvPowerSeries Algebra.toSMul MvPowerSeries.instCommSemiring CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	mul_right
smul' 📖	mathematical	PowerSeries.HasSubst	MvPowerSeries Algebra.toSMul CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra	—	IsNilpotent.smul Algebra.to_smulCommClass IsScalarTower.right
smul_X 📖	mathematical	—	PowerSeries.HasSubst MvPowerSeries Algebra.toSMul CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra MvPowerSeries.X	—	smul' X
smul_X' 📖	mathematical	—	PowerSeries.HasSubst PowerSeries Algebra.toSMul CommRing.toCommSemiring PowerSeries.instSemiring CommSemiring.toSemiring PowerSeries.instAlgebra PowerSeries.X	—	smul' X'
zero 📖	mathematical	—	PowerSeries.HasSubst MvPowerSeries MvPowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	PowerSeries.hasSubst_iff MvPowerSeries.HasSubst.zero
zero' 📖	mathematical	—	PowerSeries.HasSubst PowerSeries PowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	zero

---

← Back to Index