Expand

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

Statistics

Metric	Count
Definitions expand	1
Theorems coeff_expand, coeff_expand_mul, coeff_expand_of_not_dvd, constantCoeff_expand, expand_C, expand_X, expand_apply, expand_monomial, expand_mul, expand_mul_eq_comp, expand_one, expand_one_apply, expand_smul, expand_subst, map_expand, order_expand, support_expand, support_expand_subset	18
Total	19

PowerSeries

Definitions

Name	Category	Theorems
expand 📖	CompOp	17 math math: constantCoeff_expand, coeff_expand_mul, expand_apply, order_expand, support_expand_subset, support_expand, expand_one_apply, expand_smul, expand_C, expand_mul, expand_mul_eq_comp, map_expand, coeff_expand_of_not_dvd, expand_monomial, coeff_expand, expand_one, expand_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_expand 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff AlgHom instSemiring instAlgebra Algebra.id AlgHom.funLike expand MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	coeff_expand_mul coeff_expand_of_not_dvd
coeff_expand_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff AlgHom instSemiring instAlgebra Algebra.id AlgHom.funLike expand	—	coeff.eq_1 Finite.of_fintype expand.eq_1 smul_eq_mul Finsupp.smul_single MvPowerSeries.coeff_expand_smul
coeff_expand_of_not_dvd 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff AlgHom instSemiring instAlgebra Algebra.id AlgHom.funLike expand MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	coeff.eq_1 Finite.of_fintype expand.eq_1 MvPowerSeries.coeff_expand_of_not_dvd Finsupp.single_eq_same
constantCoeff_expand 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike constantCoeff AlgHom instAlgebra Algebra.id AlgHom.funLike expand	—	coeff_zero_eq_constantCoeff MulZeroClass.mul_zero coeff_expand_mul
expand_C 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	mul_one smul_eq_C_mul Finite.of_fintype expand.eq_1 AlgHom.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul instIsScalarTower IsScalarTower.right map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
expand_X 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	substAlgHom_X HasSubst.X_pow
expand_apply 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand subst MvPowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	MvPowerSeries.substAlgHom_apply MvPowerSeries.HasSubst.X_pow Finite.of_fintype
expand_monomial 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial	—	Finite.of_fintype MvPowerSeries.expand_monomial Finsupp.smul_single
expand_mul 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand	—	DFunLike.congr_fun expand_mul_eq_comp
expand_mul_eq_comp 📖	mathematical	—	expand AlgHom.comp PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id	—	AlgHom.ext Finite.of_fintype MvPowerSeries.expand_mul_eq_comp
expand_one 📖	mathematical	—	expand one_ne_zero MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne AlgHom.id PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id	—	one_ne_zero MvPowerSeries.expand_one Finite.of_fintype
expand_one_apply 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand one_ne_zero MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne	—	one_ne_zero expand_one
expand_smul 📖	mathematical	—	DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand Algebra.toSMul	—	AlgHom.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul instIsScalarTower IsScalarTower.right
expand_subst 📖	mathematical	HasSubst	DFunLike.coe AlgHom MvPowerSeries CommRing.toCommSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instAlgebra Algebra.id AlgHom.funLike MvPowerSeries.expand subst	—	subst.eq_1 MvPowerSeries.expand_subst HasSubst.const
map_expand 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike map AlgHom instAlgebra Algebra.id AlgHom.funLike expand	—	Finite.of_fintype MvPowerSeries.map_expand
order_expand 📖	mathematical	—	order CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom PowerSeries instSemiring instAlgebra Algebra.id AlgHom.funLike expand ENat AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	Finite.of_fintype order_eq_order MvPowerSeries.order_expand
support_expand 📖	mathematical	—	Function.support Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand Set.image Finsupp.instNatSMul Nat.instAddMonoid	—	Finite.of_fintype expand.eq_1 MvPowerSeries.support_expand
support_expand_subset 📖	mathematical	—	Set Finsupp MulZeroClass.toZero Nat.instMulZeroClass Set.instHasSubset Function.support NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe AlgHom PowerSeries CommRing.toCommSemiring instSemiring CommSemiring.toSemiring instAlgebra Algebra.id AlgHom.funLike expand Set.image Finsupp.instNatSMul Nat.instAddMonoid	—	Finite.of_fintype expand.eq_1 MvPowerSeries.support_expand subset_refl Set.instReflSubset

---

← Back to Index