Substitution

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

Statistics

Metric	Count
Definitions HasSubst, hasSubstIdeal, rescale, rescaleAlgHom, rescaleMonoidHom, subst, substAlgHom	7
Theorems X, X_pow, add, coeff_zero, comp, const_coeff, hasEval, mul_left, mul_right, smul, smul_X, zero, IsNilpotent_subst, coe_substAlgHom, coeff_rescale, coeff_subst, coeff_subst_finite, coeff_zero_iff, comp_subst, comp_substAlgHom, comp_subst_apply, constantCoeff_subst, constantCoeff_subst_eq_zero, continuous_subst, eval₂_subst, hasSubst_def, hasSubst_iff_hasEval_of_discreteTopology, hasSubst_of_constantCoeff_nilpotent, hasSubst_of_constantCoeff_zero, le_order_subst, le_weightedOrder_subst, le_weightedOrder_subst_of_forall_ne_zero, map_algebraMap_eq_subst_X, map_subst, rescaleAlgHom_apply, rescaleAlgHom_mul, rescaleAlgHom_one, rescale_eq_subst, rescale_homogeneous_eq_smul, rescale_mul, rescale_one, rescale_rescale, rescale_zero, rescale_zero_apply, substAlgHom_X, substAlgHom_apply, substAlgHom_coe, substAlgHom_comp_substAlgHom, substAlgHom_comp_substAlgHom_apply, substAlgHom_eq_aeval, substAlgHom_monomial, subst_X, subst_add, subst_coe, subst_comp_subst, subst_comp_subst_apply, subst_eq_eval₂, subst_monomial, subst_mul, subst_pow, subst_self, subst_smul	62
Total	69

MvPowerSeries

Definitions

Name	Category	Theorems
HasSubst 📖	CompData	10 math math: hasSubst_def, hasSubst_of_constantCoeff_nilpotent, hasSubst_of_constantCoeff_zero, hasSubst_iff_hasEval_of_discreteTopology, HasSubst.X_pow, PowerSeries.hasSubst_iff, HasSubst.smul_X, HasSubst.zero, HasSubst.X, PowerSeries.HasSubst.const
hasSubstIdeal 📖	CompOp	—
rescale 📖	CompOp	10 math math: rescaleUnit, rescale_mul, rescale_homogeneous_eq_smul, rescale_zero, rescale_rescale, coeff_rescale, rescaleAlgHom_apply, rescale_eq_subst, rescale_one, rescale_zero_apply
rescaleAlgHom 📖	CompOp	3 math math: rescaleAlgHom_one, rescaleAlgHom_mul, rescaleAlgHom_apply
rescaleMonoidHom 📖	CompOp	—
subst 📖	CompOp	27 math math: subst_pow, subst_eq_eval₂, constantCoeff_subst, subst_add, map_algebraMap_eq_subst_X, coe_substAlgHom, subst_comp_subst_apply, subst_monomial, map_subst, eval₂_subst, le_order_subst, subst_comp_subst, coeff_subst, subst_mul, continuous_subst, le_weightedOrder_subst, comp_subst_apply, expand_subst, constantCoeff_subst_eq_zero, subst_X, rescale_eq_subst, comp_subst, subst_smul, le_weightedOrder_subst_of_forall_ne_zero, subst_self, subst_coe, substAlgHom_apply
substAlgHom 📖	CompOp	13 math math: substAlgHom_X, coe_substAlgHom, expand_substAlgHom, substAlgHom_eq_aeval, HasSubst.comp, substAlgHom_comp_substAlgHom_apply, substAlgHom_coe, expand_comp_substAlgHom, substAlgHom_monomial, IsNilpotent_subst, comp_substAlgHom, substAlgHom_apply, substAlgHom_comp_substAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsNilpotent_subst 📖	mathematical	HasSubst IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike constantCoeff	AlgHom instAlgebra Algebra.id AlgHom.funLike substAlgHom	—	coe_substAlgHom constantCoeff_subst isNilpotent_finsum algebraMap_smul IsScalarTower.right smul_eq_mul mul_comm IsNilpotent.smul Algebra.to_smulCommClass IsNilpotent.map RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finsupp.ne_iff Finsupp.prod_filter_mul_prod_filter_not map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Finsupp.prod_eq_single Finsupp.filter_apply_neg pow_zero Finsupp.filter_apply_pos map_pow MonoidWithZeroHomClass.toMonoidHomClass IsNilpotent.pow_of_pos HasSubst.const_coeff
coe_substAlgHom 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom subst	—	IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval substAlgHom_eq_aeval coe_aeval subst_eq_eval₂
coeff_rescale 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff RingHom instSemiring RingHom.instFunLike rescale Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
coeff_subst 📖	mathematical	HasSubst	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff subst finsum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul Finsupp.prod CommRing.toCommMonoid instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval HasSum.map hasSum_aeval DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass WithPiTopology.continuous_coeff coe_substAlgHom HasSum.tsum_eq SummationFilter.instNeBotUnconditional LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul instIsScalarTower IsScalarTower.right tsum_eq_finsum coeff_subst_finite SummationFilter.instLeAtTopUnconditional
coeff_subst_finite 📖	mathematical	HasSubst	Set.Finite Finsupp MulZeroClass.toZero Nat.instMulZeroClass Function.support NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Finsupp.prod CommRing.toCommMonoid instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Summable.finite_support_of_discreteTopology DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst HasSum.summable IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval HasSum.map hasSum_aeval DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass WithPiTopology.continuous_coeff
coeff_zero_iff 📖	mathematical	—	Filter.Tendsto MvPowerSeries Filter.cofinite nhds WithPiTopology.instTopologicalSpace instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.Finite setOf DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff	—	nhds_discrete
comp_subst 📖	mathematical	HasSubst Continuous MvPowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe AlgHom CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra AlgHom.funLike	subst Algebra.id aeval RingHom Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike AlgHom.toRingHom IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing DiscreteTopology.instContinuousSMul HasEval.map HasSubst.hasEval	—	IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity DiscreteTopology.instContinuousSMul HasEval.map HasSubst.hasEval comp_substAlgHom AlgHom.coe_comp coe_substAlgHom
comp_substAlgHom 📖	mathematical	HasSubst Continuous MvPowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe AlgHom CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra AlgHom.funLike	AlgHom.comp Algebra.id substAlgHom aeval RingHom Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike AlgHom.toRingHom IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing DiscreteTopology.instContinuousSMul HasEval.map HasSubst.hasEval	—	AlgHom.ext IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity DiscreteTopology.instContinuousSMul HasEval.map HasSubst.hasEval WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul substAlgHom_eq_aeval DFunLike.congr_fun comp_aeval
comp_subst_apply 📖	mathematical	HasSubst Continuous MvPowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe AlgHom CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra AlgHom.funLike	subst Algebra.id aeval RingHom Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike AlgHom.toRingHom IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing DiscreteTopology.instContinuousSMul HasEval.map HasSubst.hasEval	—	IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity DiscreteTopology.instContinuousSMul HasEval.map HasSubst.hasEval comp_subst
constantCoeff_subst 📖	mathematical	HasSubst	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff subst finsum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul LinearMap RingHom.id instAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Finsupp.prod CommRing.toCommMonoid instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	coeff_subst
constantCoeff_subst_eq_zero 📖	mathematical	HasSubst DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	subst	—	constantCoeff_subst finsum_eq_zero_of_forall_eq_zero zero_smul Finsupp.ext map_finsuppProd MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow Finset.prod_eq_zero zero_pow smul_zero
continuous_subst 📖	mathematical	HasSubst	Continuous MvPowerSeries WithPiTopology.instTopologicalSpace UniformSpace.toTopologicalSpace subst	—	subst_eq_eval₂ continuous_eval₂ IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology continuous_algebraMap WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval
eval₂_subst 📖	mathematical	HasSubst HasEval UniformSpace.toTopologicalSpace	eval₂ algebraMap CommRing.toCommSemiring CommSemiring.toSemiring subst	—	instIsScalarTower IsScalarTower.right IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity DiscreteTopology.instContinuousSMul continuous_aeval HasEval.map HasSubst.hasEval coe_aeval aeval.congr_simp comp_subst_apply
hasSubst_def 📖	mathematical	—	HasSubst IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike constantCoeff Set.Finite setOf LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff	—	—
hasSubst_iff_hasEval_of_discreteTopology 📖	mathematical	—	HasSubst HasEval MvPowerSeries instCommRing WithPiTopology.instTopologicalSpace	—	—
hasSubst_of_constantCoeff_nilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike constantCoeff	HasSubst	—	Set.toFinite Subtype.finite
hasSubst_of_constantCoeff_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	HasSubst	—	hasSubst_of_constantCoeff_nilpotent
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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot order CommRing.toCommSemiring subst	—	LE.le.trans mul_le_mul_right CanonicallyOrderedAdd.toMulLeftMono order_le Nat.cast_sum Finset.mul_sum nsmul_eq_mul Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid mul_comm iInf_le_iff le_weightedOrder_subst
le_weightedOrder_subst 📖	mathematical	HasSubst	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat iInf Finsupp MulZeroClass.toZero Nat.instMulZeroClass ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidHom Nat.instSemiring AddZeroClass.toAddZero Finsupp.instAddZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat AddMonoidHom.instFunLike Finsupp.weight weightedOrder AddCommMonoid.toNatModule subst	—	le_weightedOrder coeff_subst finsum_eq_zero_of_forall_eq_zero zero_smul coeff_eq_zero_of_lt_weightedOrder LT.lt.trans_le LE.le.trans biInf_le Finset.sum_congr Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid nsmul_eq_mul le_weightedOrder_pow le_weightedOrder_prod smul_zero
le_weightedOrder_subst_of_forall_ne_zero 📖	mathematical	HasSubst	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat weightedOrder CommSemiring.toSemiring CommRing.toCommSemiring ENat.toNat MvPowerSeries subst	—	LE.le.trans weightedOrder_le Finset.sum_congr Nat.cast_sum Nat.cast_mul ne_zero_iff_weightedOrder_finite nsmul_eq_mul le_weightedOrder_subst
map_algebraMap_eq_subst_X 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike map algebraMap subst X	—	ext coeff_map coeff_subst HasSubst.X finsum_eq_single monomial_one_eq coeff_monomial_ne smul_zero coeff_monomial_same algebra_compatible_smul IsScalarTower.right smul_eq_mul mul_one
map_subst 📖	mathematical	HasSubst	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike map subst Algebra.id	—	ext coeff_subst hasSubst_of_constantCoeff_nilpotent IsNilpotent.map RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass HasSubst.const_coeff coeff_map AddMonoidHom.map_finsum coeff_subst_finite finsum_congr RingHomClass.toAddMonoidHomClass Finset.prod_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_prod MonoidWithZeroHomClass.toMonoidHomClass map_pow
rescaleAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike rescaleAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike rescale	—	substAlgHom_apply HasSubst.smul_X rescale_eq_subst
rescaleAlgHom_mul 📖	mathematical	—	rescaleAlgHom Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgHom.comp MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id	—	AlgHom.ext rescaleAlgHom_apply rescale_rescale
rescaleAlgHom_one 📖	mathematical	—	rescaleAlgHom Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AlgHom.id MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id	—	AlgHom.ext HasSubst.smul_X one_smul substAlgHom.congr_simp substAlgHom_apply subst_self
rescale_eq_subst 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike rescale subst Algebra.id Pi.smul' Algebra.toSMul instAlgebra X	—	ext coeff_rescale coeff_subst HasSubst.smul_X coeff_subst_finite finsum_eq_sum Finset.sum_congr Finset.sum_eq_single monomial_eq coeff_monomial MulZeroClass.mul_zero coeff_monomial_same mul_comm
rescale_homogeneous_eq_smul 📖	mathematical	DFunLike.coe AddMonoidHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.degree	RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring RingHom.instFunLike rescale Algebra.toSMul instAlgebra Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	ext coeff_rescale Finset.prod_congr Finset.prod_pow_eq_pow_sum map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.degree_apply MulZeroClass.mul_zero
rescale_mul 📖	mathematical	—	rescale Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.comp MvPowerSeries instSemiring	—	RingHom.ext ext coeff_rescale
rescale_one 📖	mathematical	—	rescale Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.id MvPowerSeries instSemiring	—	RingHom.ext ext coeff_rescale Finset.prod_congr one_pow Finset.prod_const_one one_mul
rescale_rescale 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring RingHom.instFunLike rescale Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	ext coeff_rescale mul_comm mul_pow Finsupp.prod_mul
rescale_zero 📖	mathematical	—	rescale Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.comp MvPowerSeries instSemiring C constantCoeff	—	RingHom.ext ext coeff_C one_mul Finset.prod_congr Finset.prod_eq_zero zero_pow MulZeroClass.zero_mul
rescale_zero_apply 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring RingHom.instFunLike rescale Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring C constantCoeff	—	rescale_zero
substAlgHom_X 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom X	—	MvPolynomial.coe_X substAlgHom_coe MvPolynomial.aeval_X
substAlgHom_apply 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom subst	—	coe_substAlgHom
substAlgHom_coe 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom MvPolynomial.toMvPowerSeries MvPolynomial MvPolynomial.commSemiring instCommSemiring MvPolynomial.algebra MvPolynomial.aeval	—	aeval_coe
substAlgHom_comp_substAlgHom 📖	mathematical	HasSubst	AlgHom.comp MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.restrictScalars 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	—	comp_aeval IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval instIsScalarTower IsScalarTower.right coe_substAlgHom continuous_subst
substAlgHom_comp_substAlgHom_apply 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom HasSubst.comp	—	DFunLike.congr_fun instIsScalarTower IsScalarTower.right HasSubst.comp substAlgHom_comp_substAlgHom
substAlgHom_eq_aeval 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom instCommRing aeval WithPiTopology.instUniformSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing WithPiTopology.instIsUniformAddGroup AddCommGroup.toAddGroup Ring.toAddCommGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology Semiring.toModule Ring.toSemiring MulOpposite MulOpposite.instRing Semiring.toOppositeModule WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval	—	IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval coe_aeval hasSubst_iff_hasEval_of_discreteTopology DiscreteUniformity.eq_bot
substAlgHom_monomial 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike substAlgHom LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial instMul RingHom RingHom.instFunLike algebraMap Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommMonoid instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	MvPolynomial.coe_monomial substAlgHom_coe MvPolynomial.aeval_monomial
subst_X 📖	mathematical	HasSubst	subst X CommSemiring.toSemiring CommRing.toCommSemiring	—	coe_substAlgHom substAlgHom_X
subst_add 📖	mathematical	HasSubst	subst MvPowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing	—	substAlgHom_apply map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
subst_coe 📖	mathematical	—	subst MvPolynomial.toMvPowerSeries CommRing.toCommSemiring DFunLike.coe AlgHom MvPolynomial MvPowerSeries CommSemiring.toSemiring MvPolynomial.commSemiring instCommSemiring MvPolynomial.algebra Algebra.id instAlgebra AlgHom.funLike MvPolynomial.aeval	—	subst_eq_eval₂ DiscreteUniformity.inst eval₂_coe MvPolynomial.aeval_def
subst_comp_subst 📖	mathematical	HasSubst	MvPowerSeries subst	—	instIsScalarTower IsScalarTower.right HasSubst.comp substAlgHom_apply substAlgHom.congr_simp coe_substAlgHom substAlgHom_comp_substAlgHom
subst_comp_subst_apply 📖	mathematical	HasSubst	subst	—	subst_comp_subst
subst_eq_eval₂ 📖	mathematical	—	subst eval₂ MvPowerSeries instCommRing WithPiTopology.instUniformSpace algebraMap CommRing.toCommSemiring CommSemiring.toSemiring instAlgebra	—	ext DiscreteUniformity.eq_bot
subst_monomial 📖	mathematical	HasSubst	subst DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial instMul RingHom instSemiring RingHom.instFunLike algebraMap instAlgebra Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommMonoid instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	coe_substAlgHom substAlgHom_monomial
subst_mul 📖	mathematical	HasSubst	subst MvPowerSeries instMul CommSemiring.toSemiring CommRing.toCommSemiring	—	substAlgHom_apply map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
subst_pow 📖	mathematical	HasSubst	subst MvPowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	substAlgHom_apply map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
subst_self 📖	mathematical	—	subst Algebra.id CommRing.toCommSemiring X CommSemiring.toSemiring MvPowerSeries	—	HasSubst.X coe_substAlgHom IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst instIsUniformAddGroupOfDiscreteUniformity WithPiTopology.instIsUniformAddGroup WithPiTopology.instCompleteSpace DiscreteUniformity.instCompleteSpace WithPiTopology.instT2Space T25Space.t2Space T3Space.t25Space instT3Space T1Space.t0Space instT1SpaceOfDiscreteTopology UniformSpace.to_regularSpace WithPiTopology.instIsTopologicalRing LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology WithPiTopology.instContinuousSMul DiscreteTopology.instContinuousSMul HasSubst.hasEval substAlgHom_eq_aeval HasEval.map continuous_id HasEval.X aeval_unique DFunLike.ext_iff
subst_smul 📖	mathematical	HasSubst	subst MvPowerSeries Algebra.toSMul instSemiring CommSemiring.toSemiring CommRing.toCommSemiring instAlgebra	—	substAlgHom_apply AlgHom.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul instIsScalarTower IsScalarTower.right

MvPowerSeries.HasSubst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X 📖	mathematical	—	MvPowerSeries.HasSubst MvPowerSeries.X CommSemiring.toSemiring CommRing.toCommSemiring	—	DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst MvPowerSeries.HasEval.X
X_pow 📖	mathematical	—	MvPowerSeries.HasSubst MvPowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring MvPowerSeries.X	—	MvPowerSeries.hasSubst_of_constantCoeff_zero map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MvPowerSeries.constantCoeff_X zero_pow
add 📖	mathematical	MvPowerSeries.HasSubst	Pi.instAdd MvPowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPowerSeries.instCommRing	—	MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst MvPowerSeries.HasEval.add IsTopologicalSemiring.toContinuousAdd MvPowerSeries.WithPiTopology.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring DiscreteTopology.topologicalRing MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology
coeff_zero 📖	mathematical	MvPowerSeries.HasSubst	Set.Finite setOf 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
comp 📖	mathematical	MvPowerSeries.HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike MvPowerSeries.substAlgHom	—	MvPowerSeries.IsNilpotent_subst const_coeff MvPowerSeries.coeff_zero_iff DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst Filter.Tendsto.comp MvPowerSeries.coe_substAlgHom map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MvPowerSeries.substAlgHom_apply Continuous.continuousAt MvPowerSeries.continuous_subst MvPowerSeries.HasEval.tendsto_zero hasEval
const_coeff 📖	mathematical	MvPowerSeries.HasSubst	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring RingHom.instFunLike MvPowerSeries.constantCoeff	—	—
hasEval 📖	mathematical	MvPowerSeries.HasSubst	MvPowerSeries.HasEval MvPowerSeries MvPowerSeries.instCommRing MvPowerSeries.WithPiTopology.instTopologicalSpace	—	MvPowerSeries.HasEval.mono MvPowerSeries.WithPiTopology.instTopologicalSpace_mono bot_le MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology
mul_left 📖	mathematical	MvPowerSeries.HasSubst	Pi.instMul MvPowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring	—	MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst MvPowerSeries.HasEval.mul_left MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite IsLinearTopology.instOfDiscreteTopology
mul_right 📖	mathematical	MvPowerSeries.HasSubst	Pi.instMul MvPowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring	—	mul_left mul_comm
smul 📖	mathematical	MvPowerSeries.HasSubst	MvPowerSeries Function.hasSMul Algebra.toSMul MvPowerSeries.instCommSemiring CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	mul_left
smul_X 📖	mathematical	—	MvPowerSeries.HasSubst Pi.smul' MvPowerSeries Algebra.toSMul CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id MvPowerSeries.X	—	algebra_compatible_smul IsScalarTower.right mul_left X
zero 📖	mathematical	—	MvPowerSeries.HasSubst MvPowerSeries MvPowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	DiscreteUniformity.instDiscreteTopology DiscreteUniformity.inst MvPowerSeries.HasEval.zero

---

← Back to Index