Substitution

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

Statistics

Metric	Count
Definitions HasSubst, ideal, rescaleAlgHom, subst, substAlgHom	5
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_rescaleAlgHom, coe_substAlgHom, coeff_subst, coeff_subst', coeff_subst_X_pow, coeff_subst_finite, coeff_subst_finite', constantCoeff_subst, constantCoeff_subst_X_pow, 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, rescale_eq, rescale_eq_subst, substAlgHom_X, substAlgHom_coe, substAlgHom_comp_substAlgHom, substAlgHom_comp_substAlgHom_apply, substAlgHom_eq_aeval, subst_C, subst_X, subst_add, subst_coe, subst_comp_subst, subst_comp_subst_apply, subst_def, subst_mul, subst_pow, subst_rescale_of_degree_eq_one, subst_smul, subst_sub	61
Total	66

MvPowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rescaleUnit 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike PowerSeries.rescale MvPowerSeries rescale	—	PowerSeries.rescale_eq

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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.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	19 math math: HasSubst.mul_right, HasSubst.zero, HasSubst.smul', HasSubst.X', HasSubst.X_pow, HasSubst.of_constantCoeff_zero', HasSubst.smul_X', HasSubst.zero', HasSubst.X, HasSubst.monomial', hasSubst_iff, HasSubst.add, HasSubst.mul_left, HasSubst.of_constantCoeff_zero, HasSubst.comp, HasSubst.smul, HasSubst.monomial, HasSubst.smul_X, hasSubst_iff_hasEval_of_discreteTopology
rescaleAlgHom 📖	CompOp	1 math math: coe_rescaleAlgHom
subst 📖	CompOp	31 math math: rescale_eq_subst, constantCoeff_subst, le_order_subst_left', expand_subst, expand_apply, subst_sub, subst_rescale_of_degree_eq_one, subst_mul, coeff_subst, subst_pow, le_order_subst_right', constantCoeff_subst_eq_zero, map_subst, subst_C, map_algebraMap_eq_subst_X, subst_coe, subst_add, le_order_subst, subst_def, subst_comp_subst_apply, coeff_subst_X_pow, subst_X, coeff_subst', derivative_subst, le_order_subst_right, subst_smul, constantCoeff_subst_X_pow, 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_rescaleAlgHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom PowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass rescaleAlgHom rescale	—	RingHom.ext AlgHomClass.toRingHomClass AlgHom.algHomClass ext rescale_eq RingHom.coe_coe MvPowerSeries.rescaleAlgHom_apply
coe_substAlgHom 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id 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 coeff Monoid.toPow 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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff subst finsum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring	—	coeff_subst
coeff_subst_X_pow 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff subst MvPowerSeries Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring X RingHom RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	coeff_subst' HasSubst.X_pow finsum_eq_single pow_mul coeff_X_pow Mathlib.Tactic.Contrapose.contrapose₄ Ne.pos Nat.instCanonicallyOrderedAdd smul_zero coeff_X_pow_self Algebra.algebraMap_eq_smul_one finsum_eq_zero_of_forall_eq_zero
coeff_subst_finite 📖	mathematical	HasSubst	Function.HasFiniteSupport 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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff MvPowerSeries MvPowerSeries.coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring	—	Function.HasFiniteSupport.eq_1 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	Function.HasFiniteSupport 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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.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 MvPowerSeries.instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	coeff_subst
constantCoeff_subst_X_pow 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff subst MvPowerSeries Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X algebraMap	—	coeff_zero_eq_constantCoeff coeff_subst_X_pow dvd_zero
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 constantCoeff	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike MvPowerSeries.constantCoeff subst MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	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 instLEENat 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 instReflLe 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 instLEENat order CommSemiring.toSemiring CommRing.toCommSemiring 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 MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ENat instLEENat order CommSemiring.toSemiring CommRing.toCommSemiring 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 constantCoeff	ENat instLEENat MvPowerSeries.order CommSemiring.toSemiring CommRing.toCommSemiring 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 MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	ENat instLEENat order CommSemiring.toSemiring CommRing.toCommSemiring subst Algebra.id	—	order_eq_order le_order_subst_right
le_weightedOrder_subst 📖	mathematical	HasSubst	ENat instLEENat 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 instReflLe MvPowerSeries.le_weightedOrder_subst hasSubst_iff
map_algebraMap_eq_subst_X 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.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 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
rescale_eq 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike rescale MvPowerSeries MvPowerSeries.rescale	—	ext coeff_rescale coeff.eq_1 MvPowerSeries.coeff_rescale Finsupp.prod_single_index pow_zero
rescale_eq_subst 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike rescale subst Algebra.id Algebra.toSMul MvPowerSeries.instAlgebra X	—	rescale_eq MvPowerSeries.rescale_eq_subst X.eq_1 subst.eq_1 Pi.smul_def'
substAlgHom_X 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike substAlgHom X	—	Polynomial.coe_X substAlgHom_coe Polynomial.aeval_X
substAlgHom_coe 📖	mathematical	HasSubst	DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id 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 MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.restrictScalars MvPowerSeries.instIsScalarTower NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.toSMul IsScalarTower.right 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 MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike substAlgHom HasSubst.comp	—	DFunLike.congr_fun MvPowerSeries.instIsScalarTower IsScalarTower.right 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_C 📖	mathematical	—	subst Algebra.id CommRing.toCommSemiring DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPowerSeries.instSemiring RingHom.instFunLike C MvPowerSeries MvPowerSeries.C	—	MvPowerSeries.subst_C
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 MvPowerSeries.instCommRing MvPowerSeries	—	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	—	MvPowerSeries.instIsScalarTower IsScalarTower.right HasSubst.comp coe_substAlgHom substAlgHom.congr_simp substAlgHom_comp_substAlgHom
subst_comp_subst_apply 📖	mathematical	HasSubst	subst	—	subst_comp_subst
subst_def 📖	mathematical	—	subst MvPowerSeries.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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring MvPowerSeries	—	coe_substAlgHom map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
subst_rescale_of_degree_eq_one 📖	mathematical	DFunLike.coe AddMonoidHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.degree	subst Algebra.id CommRing.toCommSemiring DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring RingHom.instFunLike rescale MvPowerSeries MvPowerSeries.rescale	—	HasSubst.of_constantCoeff_zero MvPowerSeries.coeff_zero_eq_constantCoeff_apply MvPowerSeries.coeff_apply rescale_eq_subst MvPowerSeries.rescale_eq_subst subst_comp_subst_apply IsScalarTower.right HasSubst.smul_X' subst.eq_1 MvPowerSeries.subst_comp_subst_apply HasSubst.const MvPowerSeries.HasSubst.smul_X subst_smul Polynomial.coe_X subst_coe Polynomial.aeval_X MvPowerSeries.rescale_homogeneous_eq_smul pow_one
subst_smul 📖	mathematical	HasSubst	subst PowerSeries Algebra.toSMul CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra MvPowerSeries	—	coe_substAlgHom AlgHom.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul MvPowerSeries.instIsScalarTower IsScalarTower.right
subst_sub 📖	mathematical	HasSubst	subst PowerSeries SubNegMonoid.toSub AddGroup.toSubNegMonoid MvPowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPowerSeries	—	coe_substAlgHom map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass

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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.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	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	PowerSeries.HasSubst DFunLike.coe AlgHom PowerSeries MvPowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id 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
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 MvPowerSeries.instAddCommMonoid Semiring.toModule MvPowerSeries.instModule LinearMap.instFunLike PowerSeries.monomial	—	monomial Finsupp.single_ne_zero
mul_left 📖	mathematical	PowerSeries.HasSubst	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	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 MvPowerSeries.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	PowerSeries.HasSubst MvPowerSeries Algebra.toSMul MvPowerSeries.instCommSemiring CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	mul_right
smul' 📖	mathematical	PowerSeries.HasSubst	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 MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.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 MvPowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	zero

---

← Back to Index