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`, `map`, `mul_left`, `mul_right`, `pow`, `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_C`, `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`, `subst_sub`	66
Total	73

MvPowerSeries

Definitions

Name	Category	Theorems
`HasSubst` 📖	CompData	18 math math: `hasSubst_def`, `HasSubst.map`, `hasSubst_of_constantCoeff_nilpotent`, `hasSubst_of_constantCoeff_zero`, `HasSubst.comp`, `HasSubst.mul_right`, `hasSubst_iff_hasEval_of_discreteTopology`, `HasSubst.X_pow`, `PowerSeries.hasSubst_iff`, `HasSubst.add`, `HasSubst.smul`, `HasSubst.smul_X`, `HasSubst.zero`, `HasSubst.X`, `HasSubst.pow`, `PowerSeries.HasSubst.const`, `HasSubst.expand`, `HasSubst.mul_left`
`hasSubstIdeal` 📖	CompOp	—
`rescale` 📖	CompOp	12 math math: `rescaleUnit`, `PowerSeries.subst_rescale_of_degree_eq_one`, `rescale_mul`, `rescale_homogeneous_eq_smul`, `rescale_zero`, `rescale_rescale`, `coeff_rescale`, `rescaleAlgHom_apply`, `rescale_eq_subst`, `PowerSeries.rescale_eq`, `rescale_one`, `rescale_zero_apply`
`rescaleAlgHom` 📖	CompOp	3 math math: `rescaleAlgHom_one`, `rescaleAlgHom_mul`, `rescaleAlgHom_apply`
`rescaleMonoidHom` 📖	CompOp	—
`subst` 📖	CompOp	30 math math: `subst_pow`, `subst_eq_eval₂`, `constantCoeff_subst`, `subst_add`, `subst_C`, `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`, `PowerSeries.subst_def`, `subst_X`, `rescale_eq_subst`, `comp_subst`, `subst_sub`, `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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `constantCoeff`	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toPow` `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.toPow` `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.toPow` `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`	`Function.HasFiniteSupport` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`Summable.hasFiniteSupport_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`	`MvPowerSeries` `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` `UniformSpace.toTopologicalSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DiscreteTopology.topologicalRing` `DiscreteUniformity.instDiscreteTopology` `instIsUniformAddGroupOfDiscreteUniformity` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DiscreteTopology.instContinuousSMul` `HasEval.map` `WithPiTopology.instTopologicalSpace` `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` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `substAlgHom` `aeval` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instCommRing` `RingHom.instFunLike` `AlgHom.toRingHom` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DiscreteTopology.topologicalRing` `DiscreteUniformity.instDiscreteTopology` `instIsUniformAddGroupOfDiscreteUniformity` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DiscreteTopology.instContinuousSMul` `HasEval.map` `WithPiTopology.instTopologicalSpace` `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`	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `AlgHom.funLike` `subst` `Algebra.id` `aeval` `RingHom` `Semiring.toNonAssocSemiring` `instCommRing` `RingHom.instFunLike` `AlgHom.toRingHom` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DiscreteTopology.topologicalRing` `DiscreteUniformity.instDiscreteTopology` `instIsUniformAddGroupOfDiscreteUniformity` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DiscreteTopology.instContinuousSMul` `HasEval.map` `WithPiTopology.instTopologicalSpace` `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.toPow` `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`	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `constantCoeff` `subst` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`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.toPow` `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.toPow` `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` `instLEENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `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` `instLEENat` `iInf` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `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` `instReflLe` `le_weightedOrder_pow` `le_weightedOrder_prod` `smul_zero`
`le_weightedOrder_subst_of_forall_ne_zero` 📖	mathematical	`HasSubst`	`ENat` `instLEENat` `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` `instReflLe` `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.map` `coeff_map` `AddMonoidHom.map_finsum` `coeff_subst_finite` `finsum_congr` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.prod_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `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`	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `rescale` `Algebra.toSMul` `instAlgebra` `Algebra.id` `Monoid.toPow` `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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `instCommSemiring` `AddMonoidAlgebra.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` `Ring.toSemiring` `CommRing.toRing` `aeval` `WithPiTopology.instUniformSpace` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DiscreteTopology.topologicalRing` `DiscreteUniformity.instDiscreteTopology` `instIsUniformAddGroupOfDiscreteUniformity` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `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` `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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`MvPolynomial.coe_monomial` `substAlgHom_coe` `MvPolynomial.aeval_monomial`
`subst_C` 📖	mathematical	—	`subst` `Algebra.id` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `C`	—	`eval₂_C` `algebraMap_apply`
`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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `instCommSemiring` `AddMonoidAlgebra.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` `Ring.toSemiring` `CommRing.toRing`	—	`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.toPow` `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.toPow` `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`
`subst_sub` 📖	mathematical	`HasSubst`	`subst` `MvPowerSeries` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`substAlgHom_apply` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`

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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MvPowerSeries.X`	—	`pow` `X`
`add` 📖	mathematical	`MvPowerSeries.HasSubst`	`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` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `MvPowerSeries.WithPiTopology.instIsTopologicalRing` `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`	`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.toPow` `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`
`map` 📖	mathematical	`MvPowerSeries.HasSubst`	`MvPowerSeries.HasSubst` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `MvPowerSeries.map`	—	`IsNilpotent.map` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `const_coeff` `Set.Finite.subset` `coeff_zero`
`mul_left` 📖	mathematical	`MvPowerSeries.HasSubst`	`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`	`MvPowerSeries.HasSubst` `Pi.instMul` `MvPowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`mul_left` `mul_comm`
`pow` 📖	mathematical	`MvPowerSeries.HasSubst`	`MvPowerSeries.HasSubst` `Pi.instPow` `MvPowerSeries` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Ideal.pow_mem_of_mem`
`smul` 📖	mathematical	`MvPowerSeries.HasSubst`	`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