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	MvPolynomial.IsHomogeneous DFunLike.coe Derivation MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid Semiring.toModule AddMonoidAlgebra.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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finset.univ AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.X DFunLike.coe Derivation AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid Semiring.toModule AddMonoidAlgebra.module Derivation.instFunLike MvPolynomial.pderiv AddMonoid.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass	—	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	MvPolynomial.IsWeightedHomogeneous AddCancelCommMonoid.toAddCommMonoid DFunLike.coe Derivation MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid Semiring.toModule AddMonoidAlgebra.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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finset.univ AddMonoid.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.instMul Finsupp.instAdd MvPolynomial.X DFunLike.coe Derivation AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid Semiring.toModule AddMonoidAlgebra.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