Expand

📁 Source: Mathlib/Algebra/MvPolynomial/Expand.lean

Statistics

Metric	Count
Definitions expand	1
Theorems aeval_comp_expand, aeval_expand, coe_expand, coeff_expand_of_not_dvd, coeff_expand_smul, coeff_expand_zero, eval_expand, eval₂Hom_comp_expand, eval₂_expand, expand_C, expand_X, expand_bind₁, expand_comp_bind₁, expand_eq_C, expand_eq_zero, expand_inj, expand_injective, expand_monomial, expand_mul, expand_mul_eq_comp, expand_ne_zero, expand_one, expand_one_apply, expand_zero, expand_zero_apply, isLocalHom_expand, map_expand, of_irreducible_expand, rename_comp_expand, rename_expand, support_expand, support_expand_subset, totalDegree_expand	33
Total	34

MvPolynomial

Definitions

Name	Category	Theorems
expand 📖	CompOp	42 math math: wittPolynomial_zmod_self, eval₂_expand, expand_X, MvPowerSeries.trunc'_expand_trunc', expand_eq_zero, map_expand, map_frobenius_expand, expand_monomial, expand_char, coeff_expand_smul, expand_C, expand_zero, support_expand_subset, rename_comp_expand, aeval_expand, MvPowerSeries.expand_eq_expand, expand_one_apply, map_expand_pow_char, expand_eq_C, MvPowerSeries.trunc'_expand, expand_injective, expand_one, expand_inj, totalDegree_expand, expand_bind₁, frobenius_zmod, expand_mul, isLocalHom_expand, support_expand, bind₁_rename_expand_wittPolynomial, expand_comp_bind₁, coeff_expand_of_not_dvd, map_iterateFrobenius_expand, aeval_comp_expand, rename_expand, coe_expand, expand_zmod, eval_expand, expand_mul_eq_comp, coeff_expand_zero, eval₂Hom_comp_expand, expand_zero_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_comp_expand 📖	mathematical	—	AlgHom.comp MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id aeval expand Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	algHom_ext expand_X map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass aeval_X
aeval_expand 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval expand Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_expand
coe_expand 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand eval₂ AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid C Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	—
coeff_expand_of_not_dvd 📖	mathematical	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike	coeff DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Mathlib.Tactic.Contrapose.contrapose₂ Finset.mem_image Finset.mem_of_subset support_expand_subset mem_support_iff
coeff_expand_smul 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instNatSMul Nat.instAddMonoid DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	induction_on' expand_monomial coeff_monomial Finsupp.instIsAddTorsionFree Nat.instIsAddTorsionFree map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass coeff_add
coeff_expand_zero 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	smul_zero coeff_expand_smul
eval_expand 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_expand
eval₂Hom_comp_expand 📖	mathematical	—	RingHom.comp MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring eval₂Hom RingHomClass.toRingHom AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass expand Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	ringHom_ext' AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ext algHom_C eval₂_C eval₂Hom_comp_C expand_X eval₂_pow eval₂_X eval₂Hom_X'
eval₂_expand 📖	mathematical	—	eval₂ DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	DFunLike.congr_fun AlgHomClass.toRingHomClass AlgHom.algHomClass eval₂Hom_comp_expand
expand_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C	—	eval₂Hom_C
expand_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand X Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂Hom_X'
expand_bind₁ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand bind₁	—	AlgHom.comp_apply expand_comp_bind₁
expand_comp_bind₁ 📖	mathematical	—	AlgHom.comp MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id expand bind₁ DFunLike.coe AlgHom AlgHom.funLike	—	algHom_ext bind₁_X_right
expand_eq_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C	—	expand_C
expand_eq_zero 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass	—	expand_injective map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
expand_inj 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	expand_injective
expand_injective 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	ext coeff_expand_smul
expand_monomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Finsupp.instNatSMul	—	expand.eq_1 bind₁_monomial monomial_eq Finsupp.prod_of_support_subset Finsupp.support_smul pow_zero Finset.prod_congr pow_mul
expand_mul 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	DFunLike.congr_fun expand_mul_eq_comp
expand_mul_eq_comp 📖	mathematical	—	expand AlgHom.comp MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id	—	algHom_ext expand_X pow_mul map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
expand_ne_zero 📖	—	—	—	—	Iff.not expand_eq_zero
expand_one 📖	mathematical	—	expand AlgHom.id MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id	—	algHom_ext expand_X pow_one
expand_one_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	expand_one
expand_zero 📖	mathematical	—	expand AlgHom.comp MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Algebra.ofId aeval Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	algHom_ext expand_X pow_zero eval_X
expand_zero_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C eval Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	expand_zero
isLocalHom_expand 📖	mathematical	—	IsLocalHom MvPolynomial CommRing.toCommSemiring AlgHom AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike expand	—	isUnit_iff coeff_expand_zero coeff_expand_smul Finsupp.instIsAddTorsionFree Nat.instIsAddTorsionFree
map_expand 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	map_bind₁ map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_X
of_irreducible_expand 📖	mathematical	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgHom AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid	—	isLocalHom_expand Irreducible.of_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
rename_comp_expand 📖	mathematical	—	AlgHom.comp MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id rename expand	—	algHom_ext expand_X map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass rename_X
rename_expand 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike rename expand	—	DFunLike.congr_fun rename_comp_expand
support_expand 📖	mathematical	—	support DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Finset.image Finsupp.instDecidableEq Finsupp.instNatSMul	—	HasSubset.Subset.antisymm Finset.instAntisymmSubset support_expand_subset coeff_expand_smul
support_expand_subset 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand Finset.image Finsupp.instDecidableEq Finsupp.instNatSMul	—	as_sum map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Finset.sum_congr expand_monomial HasSubset.Subset.trans Finset.instIsTransSubset support_sum coeff_monomial
totalDegree_expand 📖	mathematical	—	totalDegree DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike expand	—	expand_zero totalDegree_C MulZeroClass.mul_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass totalDegree_zero MulZeroClass.zero_mul totalDegree_eq support_expand Finsupp.card_toMultiset Finset.sup_image Finset.sup_mul₀ Nat.instCanonicallyOrderedAdd Finsupp.sum_of_support_subset Finsupp.support_smul Finset.sum_congr mul_comm Finset.sum_mul

---

← Back to Index