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 CommSemiring.toSemiring commSemiring algebra Algebra.id aeval expand Pi.instPow Monoid.toNatPow 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval expand Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_expand
coe_expand 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand eval₂ C Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	—
coeff_expand_of_not_dvd 📖	mathematical	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike	coeff AlgHom MvPolynomial CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand	—	smul_zero coeff_expand_smul
eval_expand 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval AlgHom algebra Algebra.id AlgHom.funLike expand Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_expand
eval₂Hom_comp_expand 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring eval₂Hom RingHomClass.toRingHom AlgHom algebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass expand Pi.instPow Monoid.toNatPow 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	DFunLike.congr_fun AlgHomClass.toRingHomClass AlgHom.algHomClass eval₂Hom_comp_expand
expand_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	eval₂Hom_C
expand_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂Hom_X'
expand_bind₁ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand bind₁	—	AlgHom.comp_apply expand_comp_bind₁
expand_comp_bind₁ 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id expand bind₁ DFunLike.coe AlgHom AlgHom.funLike	—	algHom_ext bind₁_X_right
expand_eq_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	expand_C
expand_eq_zero 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	expand_injective map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
expand_inj 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand	—	expand_injective
expand_injective 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand	—	ext coeff_expand_smul
expand_monomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instNatSMul Nat.instAddMonoid	—	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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand	—	DFunLike.congr_fun expand_mul_eq_comp
expand_mul_eq_comp 📖	mathematical	—	expand AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring algebra Algebra.id	—	algHom_ext expand_X pow_one
expand_one_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand	—	expand_one
expand_zero 📖	mathematical	—	expand AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C eval Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	expand_zero
isLocalHom_expand 📖	mathematical	—	IsLocalHom MvPolynomial CommRing.toCommSemiring AlgHom CommSemiring.toSemiring commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map AlgHom algebra Algebra.id AlgHom.funLike expand	—	map_bind₁ map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_X
of_irreducible_expand 📖	—	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring DFunLike.coe AlgHom algebra Algebra.id AlgHom.funLike expand	—	—	isLocalHom_expand Irreducible.of_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
rename_comp_expand 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename expand	—	DFunLike.congr_fun rename_comp_expand
support_expand 📖	mathematical	—	support DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand Finset.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instDecidableEq Finsupp.instNatSMul Nat.instAddMonoid	—	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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike expand Finset.image Finsupp.instDecidableEq Finsupp.instNatSMul Nat.instAddMonoid	—	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 CommSemiring.toSemiring commSemiring 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