EulerIdentity

📁 Source: Mathlib/RingTheory/MvPolynomial/EulerIdentity.lean

Statistics

Metric	Count
Definitions	0
Theorems pderiv, sum_X_mul_pderiv, pderiv, sum_weight_X_mul_pderiv	4
Total	4

MvPolynomial.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pderiv 📖	mathematical	MvPolynomial.IsHomogeneous	DFunLike.coe Derivation MvPolynomial MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv	—	MvPolynomial.totalDegree_eq_zero_iff_eq_C MvPolynomial.totalDegree_zero_iff_isHomogeneous MvPolynomial.pderiv_C MvPolynomial.isHomogeneous_zero MvPolynomial.IsWeightedHomogeneous.pderiv
sum_X_mul_pderiv 📖	mathematical	MvPolynomial.IsHomogeneous	Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MvPolynomial.X DFunLike.coe Derivation MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv Finset.sum_congr one_smul

MvPolynomial.IsWeightedHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pderiv 📖	mathematical	MvPolynomial.IsWeightedHomogeneous AddCancelCommMonoid.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	DFunLike.coe Derivation MvPolynomial MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv	—	Submodule.span_induction Nat.instCanonicallyOrderedAdd Nat.instOrderedSub MvPolynomial.pderiv_monomial one_mul Nat.cast_zero MvPolynomial.monomial_zero MvPolynomial.isWeightedHomogeneous_zero MvPolynomial.isWeightedHomogeneous_monomial add_right_cancel_iff AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.weight_sub_single_add map_zero AddMonoidHomClass.toZeroHomClass Derivation.instAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass add Derivation.map_smul Submodule.smul_mem Finsupp.supported_eq_span_single MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported MvPolynomial.mem_weightedHomogeneousSubmodule
sum_weight_X_mul_pderiv 📖	mathematical	MvPolynomial.IsWeightedHomogeneous Nat.instAddCommMonoid	Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring Finset.univ AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MvPolynomial.X DFunLike.coe Derivation MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv	—	Submodule.span_induction Finset.sum_congr MvPolynomial.X_mul_pderiv_monomial smul_smul mul_comm Finsupp.sum_fintype zero_smul Finsupp.weight_apply Set.mem_setOf map_zero AddMonoidHomClass.toZeroHomClass Derivation.instAddMonoidHomClass MulZeroClass.mul_zero nsmul_zero Finset.sum_const_zero map_add AddMonoidHomClass.toAddHomClass left_distrib Distrib.leftDistribClass smul_add Finset.sum_add_distrib Derivation.map_smul nsmul_eq_mul mul_smul_comm Algebra.to_smulCommClass Finsupp.supported_eq_span_single MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported MvPolynomial.mem_weightedHomogeneousSubmodule

---

← Back to Index