WeightedHomogeneous

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

Statistics

Metric	Count
Definitions `IsWeightedHomogeneous`, `NonTorsionWeight`, `decompose'`, `weightedDecomposition`, `weightedGradedAlgebra`, `weightedHomogeneousComponent`, `weightedHomogeneousSubmodule`, `weightedTotalDegree`, `weightedTotalDegree'`	9
Theorems `coeAddMonoidHom_eq_support_sum`, `coeLinearMap_eq_dfinsuppSum`, `coeLinearMap_eq_finsum`, `C_mul`, `add`, `coeff_eq_zero`, `induction_on`, `inj_right`, `mul`, `pow`, `prod`, `sum`, `weightedHomogeneousComponent_ne`, `weightedHomogeneousComponent_same`, `weighted_total_degree`, `gradedMonoid`, `coeff_weightedHomogeneousComponent`, `decompose'_apply`, `finsum_weightedHomogeneousComponent`, `isWeightedHomogeneous_C`, `isWeightedHomogeneous_X`, `isWeightedHomogeneous_monomial`, `isWeightedHomogeneous_of_total_degree_zero`, `isWeightedHomogeneous_one`, `isWeightedHomogeneous_zero`, `isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero`, `le_weightedTotalDegree`, `mem_weightedHomogeneousSubmodule`, `nonTorsionWeight_of`, `sum_weightedHomogeneousComponent`, `decompose'_apply`, `decompose'_eq`, `weightedDegree_eq_zero_iff`, `weightedHomogeneousComponent_C_mul`, `weightedHomogeneousComponent_apply`, `weightedHomogeneousComponent_directSum`, `weightedHomogeneousComponent_eq_zero`, `weightedHomogeneousComponent_eq_zero'`, `weightedHomogeneousComponent_eq_zero_of_notMem`, `weightedHomogeneousComponent_finsupp`, `weightedHomogeneousComponent_isWeightedHomogeneous`, `weightedHomogeneousComponent_mem`, `weightedHomogeneousComponent_of_isWeightedHomogeneous_ne`, `weightedHomogeneousComponent_of_isWeightedHomogeneous_same`, `weightedHomogeneousComponent_of_mem`, `weightedHomogeneousComponent_zero`, `weightedHomogeneousSubmodule_eq_finsupp_supported`, `weightedHomogeneousSubmodule_mul`, `weightedTotalDegree'_eq_bot_iff`, `weightedTotalDegree'_zero`, `weightedTotalDegree_coe`, `weightedTotalDegree_eq_zero_iff`, `weightedTotalDegree_zero`	53
Total	62

MvPolynomial

Definitions

Name	Category	Theorems
`IsWeightedHomogeneous` 📖	MathDef	9 math math: `isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero`, `isWeightedHomogeneous_one`, `isWeightedHomogeneous_monomial`, `isWeightedHomogeneous_zero`, `mem_weightedHomogeneousSubmodule`, `weightedHomogeneousComponent_isWeightedHomogeneous`, `isWeightedHomogeneous_X`, `isWeightedHomogeneous_of_total_degree_zero`, `isWeightedHomogeneous_C`
`NonTorsionWeight` 📖	MathDef	1 math math: `nonTorsionWeight_of`
`decompose'` 📖	CompOp	1 math math: `decompose'_apply`
`weightedDecomposition` 📖	CompOp	2 math math: `weightedDecomposition.decompose'_apply`, `weightedDecomposition.decompose'_eq`
`weightedGradedAlgebra` 📖	CompOp	—
`weightedHomogeneousComponent` 📖	CompOp	21 math math: `weightedHomogeneousComponent_of_isWeightedHomogeneous_same`, `IsWeightedHomogeneous.weightedHomogeneousComponent_same`, `weightedHomogeneousComponent_zero`, `weightedDecomposition.decompose'_apply`, `weightedHomogeneousComponent_eq_zero'`, `IsWeightedHomogeneous.weightedHomogeneousComponent_ne`, `sum_weightedHomogeneousComponent`, `decompose'_apply`, `weightedHomogeneousComponent_directSum`, `weightedHomogeneousComponent_finsupp`, `weightedHomogeneousComponent_of_isWeightedHomogeneous_ne`, `weightedHomogeneousComponent_isWeightedHomogeneous`, `weightedHomogeneousComponent_eq_zero_of_notMem`, `weightedDecomposition.decompose'_eq`, `weightedHomogeneousComponent_eq_zero`, `weightedHomogeneousComponent_C_mul`, `weightedHomogeneousComponent_mem`, `weightedHomogeneousComponent_of_mem`, `coeff_weightedHomogeneousComponent`, `finsum_weightedHomogeneousComponent`, `weightedHomogeneousComponent_apply`
`weightedHomogeneousSubmodule` 📖	CompOp	13 math math: `DirectSum.coeLinearMap_eq_dfinsuppSum`, `weightedHomogeneousSubmodule_mul`, `weightedDecomposition.decompose'_apply`, `weightedHomogeneousSubmodule_eq_finsupp_supported`, `DirectSum.coeAddMonoidHom_eq_support_sum`, `decompose'_apply`, `weightedHomogeneousComponent_directSum`, `mem_weightedHomogeneousSubmodule`, `weightedHomogeneousSubmodule_one`, `DirectSum.coeLinearMap_eq_finsum`, `weightedDecomposition.decompose'_eq`, `weightedHomogeneousComponent_mem`, `WeightedHomogeneousSubmodule.gradedMonoid`
`weightedTotalDegree` 📖	CompOp	7 math math: `isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero`, `le_weightedTotalDegree`, `weightedTotalDegree_eq_zero_iff`, `weightedTotalDegree_one`, `weightedTotalDegree_coe`, `weightedTotalDegree_rename_of_injective`, `weightedTotalDegree_zero`
`weightedTotalDegree'` 📖	CompOp	4 math math: `weightedTotalDegree_coe`, `weightedTotalDegree'_zero`, `IsWeightedHomogeneous.weighted_total_degree`, `weightedTotalDegree'_eq_bot_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_weightedHomogeneousComponent` 📖	mathematical	—	`coeff` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`Finsupp.filter_apply`
`decompose'_apply` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `weightedHomogeneousSubmodule` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `decompose'` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`decompose'.eq_1` `DirectSum.mk_apply_of_mem` `DirectSum.mk_apply_of_notMem` `Submodule.coe_zero` `weightedHomogeneousComponent_eq_zero_of_notMem`
`finsum_weightedHomogeneousComponent` 📖	mathematical	—	`finsum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`sum_weightedHomogeneousComponent`
`isWeightedHomogeneous_C` 📖	mathematical	—	`IsWeightedHomogeneous` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`isWeightedHomogeneous_monomial` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`isWeightedHomogeneous_X` 📖	mathematical	—	`IsWeightedHomogeneous` `X`	—	`isWeightedHomogeneous_monomial` `Finsupp.linearCombination_single` `one_nsmul`
`isWeightedHomogeneous_monomial` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	`IsWeightedHomogeneous` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`coeff_monomial`
`isWeightedHomogeneous_of_total_degree_zero` 📖	mathematical	`weightedTotalDegree` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsWeightedHomogeneous`	—	`weightedTotalDegree_coe` `ne_zero_iff` `eq_bot_iff` `WithBot.coe_le_coe` `Finset.le_sup` `mem_support_iff`
`isWeightedHomogeneous_one` 📖	mathematical	—	`IsWeightedHomogeneous` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`isWeightedHomogeneous_C`
`isWeightedHomogeneous_zero` 📖	mathematical	—	`IsWeightedHomogeneous` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Submodule.zero_mem`
`isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero` 📖	mathematical	—	`IsWeightedHomogeneous` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `weightedTotalDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`weightedTotalDegree.eq_1` `bot_eq_zero` `Finset.sup_eq_bot_iff` `IsWeightedHomogeneous.eq_1` `mem_support_iff`
`le_weightedTotalDegree` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `support`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `DFunLike.coe` `AddMonoidHom` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `weightedTotalDegree`	—	`Finset.le_sup`
`mem_weightedHomogeneousSubmodule` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `weightedHomogeneousSubmodule` `IsWeightedHomogeneous`	—	—
`nonTorsionWeight_of` 📖	mathematical	—	`NonTorsionWeight`	—	`smul_eq_zero_iff_left` `IsAddTorsionFree.to_isTorsionFree_nat` `Nat.instIsCancelMulZero`
`sum_weightedHomogeneousComponent` 📖	mathematical	—	`finsum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`weightedHomogeneousComponent_finsupp` `finsum_eq_sum` `ext` `coeff_sum` `Finset.sum_congr` `coeff_weightedHomogeneousComponent` `Finset.sum_eq_single` `coeff_zero`
`weightedDegree_eq_zero_iff` 📖	mathematical	`NonTorsionWeight`	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `AddZero.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`Finsupp.sum.eq_1` `Finset.sum_eq_zero_iff` `Unique.instSubsingleton` `Finsupp.mem_support_iff` `le_antisymm` `le_trans` `le_of_eq` `le_refl` `ge_of_eq`
`weightedHomogeneousComponent_C_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `C`	—	`C_mul'` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`weightedHomogeneousComponent_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nat.instSemiring` `Finset.filter` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `support` `monomial` `coeff`	—	`Finsupp.filter_eq_sum` `Finset.sum_congr` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`weightedHomogeneousComponent_directSum` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `DirectSum` `Submodule` `SetLike.instMembership` `Submodule.setLike` `weightedHomogeneousSubmodule` `Submodule.addCommMonoid` `instAddCommMonoidDirectSum` `DirectSum.instModule` `Submodule.module` `DirectSum.coeLinearMap` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike`	—	`DirectSum.coeLinearMap_eq_dfinsuppSum` `DFinsupp.sum.eq_1` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `IsWeightedHomogeneous.weightedHomogeneousComponent_same` `Subtype.prop` `Finset.sum_eq_single` `IsWeightedHomogeneous.weightedHomogeneousComponent_ne` `DFinsupp.notMem_support_iff` `Submodule.coe_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`weightedHomogeneousComponent_eq_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `weightedTotalDegree`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`weightedHomogeneousComponent_apply` `Finset.sum_eq_zero` `lt_irrefl` `Finset.mem_filter` `lt_of_le_of_lt` `le_weightedTotalDegree`
`weightedHomogeneousComponent_eq_zero'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`weightedHomogeneousComponent_apply` `Finset.sum_eq_zero` `Finset.mem_filter`
`weightedHomogeneousComponent_eq_zero_of_notMem` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.image` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `support`	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`weightedHomogeneousComponent_eq_zero'` `mem_support_iff`
`weightedHomogeneousComponent_finsupp` 📖	mathematical	—	`Set.Finite` `Function.support` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`Set.Finite.subset` `Set.toFinite` `Finite.Set.finite_image` `Finite.of_fintype` `weightedHomogeneousComponent_eq_zero'`
`weightedHomogeneousComponent_isWeightedHomogeneous` 📖	mathematical	—	`IsWeightedHomogeneous` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `coeff_weightedHomogeneousComponent`
`weightedHomogeneousComponent_mem` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `weightedHomogeneousSubmodule` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`mem_weightedHomogeneousSubmodule` `weightedHomogeneousComponent_isWeightedHomogeneous`
`weightedHomogeneousComponent_of_isWeightedHomogeneous_ne` 📖	mathematical	`IsWeightedHomogeneous`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsWeightedHomogeneous.weightedHomogeneousComponent_ne`
`weightedHomogeneousComponent_of_isWeightedHomogeneous_same` 📖	mathematical	`IsWeightedHomogeneous`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`IsWeightedHomogeneous.weightedHomogeneousComponent_same`
`weightedHomogeneousComponent_of_mem` 📖	mathematical	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `weightedHomogeneousSubmodule`	`DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `weightedHomogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`ext` `coeff_weightedHomogeneousComponent`
`weightedHomogeneousComponent_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `RingHom` `RingHom.instFunLike` `C` `coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`ext` `coeff_weightedHomogeneousComponent` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `coeff_zero_C` `Finset.sum_congr` `Unique.instSubsingleton` `IsAddTorsionFree.to_isTorsionFree_nat` `Nat.instIsCancelMulZero` `coeff_C`
`weightedHomogeneousSubmodule_eq_finsupp_supported` 📖	mathematical	—	`weightedHomogeneousSubmodule` `Finsupp.supported` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`Submodule.ext` `Finsupp.mem_supported` `Set.subset_def`
`weightedHomogeneousSubmodule_mul` 📖	mathematical	—	`Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.mul` `IsScalarTower.right` `algebra` `Algebra.id` `weightedHomogeneousSubmodule` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsScalarTower.right` `Submodule.mul_le` `Finset.exists_ne_zero_of_sum_ne_zero` `coeff_mul` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `Finset.HasAntidiagonal.mem_antidiagonal` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`
`weightedTotalDegree'_eq_bot_iff` 📖	mathematical	—	`weightedTotalDegree'` `Bot.bot` `WithBot` `WithBot.bot` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	—
`weightedTotalDegree'_zero` 📖	mathematical	—	`weightedTotalDegree'` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Bot.bot` `WithBot` `WithBot.bot`	—	`Finset.sup_empty`
`weightedTotalDegree_coe` 📖	mathematical	—	`weightedTotalDegree'` `WithBot.some` `weightedTotalDegree`	—	`WithBot.ne_bot_iff_exists` `weightedTotalDegree'_eq_bot_iff` `le_antisymm` `Finset.le_sup` `le_of_eq`
`weightedTotalDegree_eq_zero_iff` 📖	mathematical	`NonTorsionWeight`	`weightedTotalDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero` `IsWeightedHomogeneous.eq_1` `mem_support_iff` `weightedDegree_eq_zero_iff`
`weightedTotalDegree_zero` 📖	mathematical	—	`weightedTotalDegree` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`Finset.sup_empty`

MvPolynomial.DirectSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeAddMonoidHom_eq_support_sum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DirectSum` `MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `MvPolynomial.weightedHomogeneousSubmodule` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.coeAddMonoidHom` `DFinsupp.sum` `AddZero.toZero` `MvPolynomial.decidableEqMvPolynomial`	—	`coeLinearMap_eq_dfinsuppSum`
`coeLinearMap_eq_dfinsuppSum` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DirectSum` `MvPolynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `MvPolynomial.weightedHomogeneousSubmodule` `Submodule.addCommMonoid` `instAddCommMonoidDirectSum` `DirectSum.instModule` `Submodule.module` `LinearMap.instFunLike` `DirectSum.coeLinearMap` `DFinsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MvPolynomial.decidableEqMvPolynomial`	—	`DirectSum.coeLinearMap_eq_dfinsuppSum`
`coeLinearMap_eq_finsum` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DirectSum` `MvPolynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `MvPolynomial.weightedHomogeneousSubmodule` `Submodule.addCommMonoid` `instAddCommMonoidDirectSum` `DirectSum.instModule` `Submodule.module` `LinearMap.instFunLike` `DirectSum.coeLinearMap` `finsum` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike`	—	`coeLinearMap_eq_dfinsuppSum` `DFinsupp.sum.eq_1` `finsum_eq_sum_of_support_subset` `DirectSum.support_subset` `Submodule.addSubmonoidClass`

MvPolynomial.IsWeightedHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_mul` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `MvPolynomial.C`	—	`zero_add` `mul` `MvPolynomial.isWeightedHomogeneous_C`
`add` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Submodule.add_mem`
`coeff_eq_zero` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`MvPolynomial.coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—
`induction_on` 📖	—	`MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.isWeightedHomogeneous_zero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `add` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `MvPolynomial.isWeightedHomogeneous_monomial` `MvPolynomial.IsWeightedHomogeneous`	—	—	`MvPolynomial.isWeightedHomogeneous_zero` `add` `MvPolynomial.isWeightedHomogeneous_monomial` `C_mul` `mul_add` `Distrib.leftDistribClass` `MulZeroClass.mul_zero` `Algebra.smul_def` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Submodule.span_le` `Set.image_subset_iff` `MvPolynomial.C_mul_monomial` `mul_one` `Finsupp.supported_eq_span_single` `MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported` `MvPolynomial.mem_weightedHomogeneousSubmodule` `one_mul`
`inj_right` 📖	—	`MvPolynomial.IsWeightedHomogeneous`	—	—	`MvPolynomial.exists_coeff_ne_zero`
`mul` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`MvPolynomial.weightedHomogeneousSubmodule_mul` `Submodule.mul_mem_mul` `IsScalarTower.right`
`pow` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`pow_zero` `zero_smul` `MvPolynomial.isWeightedHomogeneous_one` `pow_succ` `succ_nsmul` `mul`
`prod` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `Finset.sum`	—	`Finset.induction_on` `Finset.prod_insert` `Finset.sum_insert` `mul` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`
`sum` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Submodule.sum_mem`
`weightedHomogeneousComponent_ne` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `MvPolynomial.weightedHomogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`MvPolynomial.ext` `MvPolynomial.coeff_weightedHomogeneousComponent` `MvPolynomial.coeff_zero`
`weightedHomogeneousComponent_same` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `MvPolynomial.weightedHomogeneousComponent`	—	`MvPolynomial.ext` `MvPolynomial.coeff_weightedHomogeneousComponent`
`weighted_total_degree` 📖	mathematical	`MvPolynomial.IsWeightedHomogeneous`	`MvPolynomial.weightedTotalDegree'` `WithBot.some`	—	`le_antisymm` `le_of_eq` `MvPolynomial.exists_coeff_ne_zero` `Finsupp.mem_support_iff` `Finset.le_sup`

MvPolynomial.WeightedHomogeneousSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gradedMonoid` 📖	mathematical	—	`SetLike.GradedMonoid` `MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `Submodule.setLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `MvPolynomial.weightedHomogeneousSubmodule`	—	`MvPolynomial.isWeightedHomogeneous_one` `MvPolynomial.IsWeightedHomogeneous.mul`

MvPolynomial.weightedDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decompose'_apply` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `MvPolynomial.weightedHomogeneousSubmodule` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum.Decomposition.decompose'` `Submodule.addSubmonoidClass` `MvPolynomial.weightedDecomposition` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `MvPolynomial.weightedHomogeneousComponent`	—	`MvPolynomial.decompose'_apply`
`decompose'_eq` 📖	mathematical	—	`DirectSum.Decomposition.decompose'` `MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Semiring.toModule` `Submodule.setLike` `Submodule.addSubmonoidClass` `MvPolynomial.weightedHomogeneousSubmodule` `MvPolynomial.weightedDecomposition` `DFunLike.coe` `AddMonoidHom` `DirectSum` `SetLike.instMembership` `Submodule.addCommMonoid` `AddZeroClass.toAddZero` `Pi.addZeroClass` `Set.Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nat.instSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `MvPolynomial.support` `Set` `Set.instMembership` `instAddCommMonoidDirectSum` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `MvPolynomial.weightedHomogeneousComponent` `MvPolynomial.weightedHomogeneousComponent_mem`	—	`Submodule.addSubmonoidClass`

---

← Back to Index