Homogeneous

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

Statistics

Metric	Count
Definitions `IsHomogeneous`, `decomposition`, `gradedAlgebra`, `homogeneousComponent`, `homogeneousSubmodule`	5
Theorems `mem_span_iff_exists_isHomogeneous`, `mem_span_pow_iff_exists_isHomogeneous`, `span_eq_map_homogeneousSubmodule`, `span_pow_eq_map_homogeneousSubmodule`, `gradedMonoid`, `C_mul`, `gcommSemiring`, `add`, `aeval`, `coeff_eq_zero`, `coeff_isHomogeneous_of_optionEquivLeft_symm`, `eq_zero_of_forall_eval_eq_zero`, `eq_zero_of_forall_eval_eq_zero_of_le_card`, `eval₂`, `finSuccEquiv_coeff_isHomogeneous`, `funext`, `funext_of_le_card`, `inj_right`, `map`, `mul`, `neg`, `of_map`, `pow`, `prod`, `rename_isHomogeneous`, `rename_isHomogeneous_iff`, `sub`, `sum`, `totalDegree`, `totalDegree_le`, `coeff_homogeneousComponent`, `decompose'_apply`, `decompose'_eq`, `homogeneousComponent_C_mul`, `homogeneousComponent_apply`, `homogeneousComponent_eq_zero`, `homogeneousComponent_eq_zero'`, `homogeneousComponent_isHomogeneous`, `homogeneousComponent_mem`, `homogeneousComponent_of_mem`, `homogeneousComponent_zero`, `homogeneousSubmodule_eq_finsupp_supported`, `homogeneousSubmodule_mul`, `homogeneousSubmodule_one_eq_span_X`, `homogeneousSubmodule_one_pow`, `homogeneousSubmodule_zero`, `isHomogeneous_C`, `isHomogeneous_C_mul_X`, `isHomogeneous_C_mul_X_pow`, `isHomogeneous_X`, `isHomogeneous_X_pow`, `isHomogeneous_monomial`, `isHomogeneous_of_totalDegree_zero`, `isHomogeneous_one`, `isHomogeneous_zero`, `mem_homogeneousSubmodule`, `monomial_mem_homogeneousSubmodule_pow_degree`, `sum_homogeneousComponent`, `totalDegree_eq_zero_iff`, `totalDegree_zero_iff_isHomogeneous`, `weightedHomogeneousSubmodule_one`, `weightedTotalDegree_one`, `weightedTotalDegree_rename_of_injective`	63
Total	68

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_span_iff_exists_isHomogeneous` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `Set.range` `MvPolynomial.IsHomogeneous` `DFunLike.coe` `RingHom` `MvPolynomial` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	`RingHomSurjective.ids` `span_eq_map_homogeneousSubmodule`
`mem_span_pow_iff_exists_isHomogeneous` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `span` `Set.range` `MvPolynomial.IsHomogeneous` `DFunLike.coe` `RingHom` `MvPolynomial` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	`IsScalarTower.right` `RingHomSurjective.ids` `span_pow_eq_map_homogeneousSubmodule`
`span_eq_map_homogeneousSubmodule` 📖	mathematical	—	`span` `CommSemiring.toSemiring` `Set.range` `Submodule.map` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `Algebra.toModule` `MvPolynomial.algebra` `Algebra.id` `RingHom.id` `RingHomSurjective.ids` `AlgHom.toLinearMap` `MvPolynomial.aeval` `MvPolynomial.homogeneousSubmodule`	—	`RingHomSurjective.ids` `Submodule.map.congr_simp` `MvPolynomial.homogeneousSubmodule_one_eq_span_X` `Submodule.map_span` `Set.image_congr` `MvPolynomial.eval_X`
`span_pow_eq_map_homogeneousSubmodule` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `span` `Set.range` `Submodule.map` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `Algebra.toModule` `MvPolynomial.algebra` `RingHom.id` `RingHomSurjective.ids` `AlgHom.toLinearMap` `MvPolynomial.aeval` `MvPolynomial.homogeneousSubmodule`	—	`IsScalarTower.right` `RingHomSurjective.ids` `MvPolynomial.homogeneousSubmodule_one_pow` `Submodule.map_pow` `span_eq_map_homogeneousSubmodule`

MvPolynomial

Definitions

Name	Category	Theorems
`IsHomogeneous` 📖	MathDef	21 math math: `Ideal.mem_span_iff_exists_isHomogeneous`, `Polynomial.isHomogeneous_homogenize`, `LinearMap.polyCharpoly_coeff_isHomogeneous`, `homogeneousComponent_isHomogeneous`, `isHomogeneous_C_mul_X`, `Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous`, `isHomogeneous_X`, `isHomogeneous_of_totalDegree_zero`, `isHomogeneous_monomial`, `Matrix.charpoly.univ_coeff_isHomogeneous`, `isHomogeneous_one`, `mem_homogeneousSubmodule`, `isHomogeneous_zero`, `IsHomogeneous.rename_isHomogeneous_iff`, `isHomogeneous_C_mul_X_pow`, `LinearMap.toMvPolynomial_isHomogeneous`, `isHomogeneous_C`, `totalDegree_zero_iff_isHomogeneous`, `Ideal.mem_span_pow_iff_exists_isHomogeneous`, `Matrix.toMvPolynomial_isHomogeneous`, `isHomogeneous_X_pow`
`decomposition` 📖	CompOp	2 math math: `decomposition.decompose'_apply`, `decomposition.decompose'_eq`
`gradedAlgebra` 📖	CompOp	—
`homogeneousComponent` 📖	CompOp	12 math math: `homogeneousComponent_eq_zero'`, `homogeneousComponent_of_mem`, `homogeneousComponent_mem`, `homogeneousComponent_C_mul`, `homogeneousComponent_isHomogeneous`, `sum_homogeneousComponent`, `coeff_homogeneousComponent`, `homogeneousComponent_apply`, `decomposition.decompose'_apply`, `homogeneousComponent_eq_zero`, `homogeneousComponent_zero`, `decomposition.decompose'_eq`
`homogeneousSubmodule` 📖	CompOp	15 math math: `homogeneousComponent_mem`, `Ideal.span_pow_eq_map_homogeneousSubmodule`, `Ideal.span_eq_map_homogeneousSubmodule`, `IsHomogeneous.HomogeneousSubmodule.gcommSemiring`, `homogeneousSubmodule_zero`, `weightedHomogeneousSubmodule_one`, `decomposition.decompose'_apply`, `mem_homogeneousSubmodule`, `monomial_mem_homogeneousSubmodule_pow_degree`, `homogeneousSubmodule_eq_finsupp_supported`, `HomogeneousSubmodule.gradedMonoid`, `homogeneousSubmodule_one_eq_span_X`, `homogeneousSubmodule_one_pow`, `homogeneousSubmodule_mul`, `decomposition.decompose'_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_homogeneousComponent` 📖	mathematical	—	`coeff` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finsupp.degree_eq_weight_one` `coeff_weightedHomogeneousComponent`
`homogeneousComponent_C_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `C`	—	`weightedHomogeneousComponent_C_mul`
`homogeneousComponent_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset.filter` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `support` `monomial` `coeff`	—	`Finset.sum_congr` `Finset.filter.congr_simp` `Finsupp.degree_eq_weight_one` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `weightedHomogeneousComponent_apply`
`homogeneousComponent_eq_zero` 📖	mathematical	`totalDegree`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`homogeneousComponent_eq_zero'` `ne_of_lt` `Finset.sup_lt_iff` `lt_of_le_of_lt` `totalDegree.eq_1`
`homogeneousComponent_eq_zero'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`weightedHomogeneousComponent_eq_zero'` `Finsupp.degree_eq_weight_one`
`homogeneousComponent_isHomogeneous` 📖	mathematical	—	`IsHomogeneous` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent`	—	`weightedHomogeneousComponent_isWeightedHomogeneous`
`homogeneousComponent_mem` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `homogeneousSubmodule` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `homogeneousComponent`	—	`weightedHomogeneousComponent_mem`
`homogeneousComponent_of_mem` 📖	mathematical	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `homogeneousSubmodule`	`DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `homogeneousComponent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`weightedHomogeneousComponent_of_mem`
`homogeneousComponent_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `RingHom` `RingHom.instFunLike` `C` `coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`weightedHomogeneousComponent_zero` `Nat.instCanonicallyOrderedAdd` `Nat.instIsAddTorsionFree`
`homogeneousSubmodule_eq_finsupp_supported` 📖	mathematical	—	`homogeneousSubmodule` `Finsupp.supported` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`Finsupp.degree_eq_weight_one` `weightedHomogeneousSubmodule_eq_finsupp_supported`
`homogeneousSubmodule_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` `homogeneousSubmodule`	—	`weightedHomogeneousSubmodule_mul`
`homogeneousSubmodule_one_eq_span_X` 📖	mathematical	—	`homogeneousSubmodule` `Submodule.span` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Set.range` `X`	—	`homogeneousSubmodule_eq_finsupp_supported` `Finsupp.supported_eq_span_single` `Set.image_congr` `pow_one`
`homogeneousSubmodule_one_pow` 📖	mathematical	—	`Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `algebra` `Algebra.id` `homogeneousSubmodule`	—	`le_antisymm` `IsScalarTower.right` `pow_zero` `homogeneousSubmodule_zero` `pow_add` `pow_one` `le_imp_le_of_le_of_le` `mul_le_mul_left` `Submodule.instMulRightMono` `le_refl` `homogeneousSubmodule_mul` `IsWeightedHomogeneous.induction_on` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Submodule.add_mem` `Finsupp.degree_eq_weight_one` `Pi.one_def` `monomial_mem_homogeneousSubmodule_pow_degree`
`homogeneousSubmodule_zero` 📖	mathematical	—	`homogeneousSubmodule` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.one`	—	`Submodule.ext` `mem_homogeneousSubmodule` `totalDegree_zero_iff_isHomogeneous` `Submodule.mem_one` `algebraMap_eq` `totalDegree_eq_zero_iff_eq_C`
`isHomogeneous_C` 📖	mathematical	—	`IsHomogeneous` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C`	—	`isHomogeneous_monomial` `Finset.sum_congr` `Finset.sum_const_zero`
`isHomogeneous_C_mul_X` 📖	mathematical	—	`IsHomogeneous` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `X`	—	`IsHomogeneous.C_mul` `isHomogeneous_X`
`isHomogeneous_C_mul_X_pow` 📖	mathematical	—	`IsHomogeneous` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`IsHomogeneous.C_mul` `isHomogeneous_X_pow`
`isHomogeneous_X` 📖	mathematical	—	`IsHomogeneous` `X`	—	`isHomogeneous_monomial` `Finset.sum_congr` `Finsupp.support_single_ne_zero` `one_ne_zero` `Finset.sum_singleton` `Finsupp.single_eq_same`
`isHomogeneous_X_pow` 📖	mathematical	—	`IsHomogeneous` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `X`	—	`one_mul` `IsHomogeneous.pow` `isHomogeneous_X`
`isHomogeneous_monomial` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	`IsHomogeneous` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`isWeightedHomogeneous_monomial` `Finsupp.degree_eq_weight_one`
`isHomogeneous_of_totalDegree_zero` 📖	mathematical	`totalDegree`	`IsHomogeneous`	—	`totalDegree_zero_iff_isHomogeneous`
`isHomogeneous_one` 📖	mathematical	—	`IsHomogeneous` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`isHomogeneous_C`
`isHomogeneous_zero` 📖	mathematical	—	`IsHomogeneous` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Submodule.zero_mem`
`mem_homogeneousSubmodule` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `homogeneousSubmodule` `IsHomogeneous`	—	—
`monomial_mem_homogeneousSubmodule_pow_degree` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instPowNat` `IsScalarTower.right` `algebra` `Algebra.id` `homogeneousSubmodule` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial`	—	`Finsupp.induction` `IsScalarTower.right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `pow_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `Finsupp.degree_single` `monomial_single_add` `pow_add` `Submodule.mul_mem_mul` `Submodule.pow_mem_pow` `isHomogeneous_X`
`sum_homogeneousComponent` 📖	mathematical	—	`Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.range` `totalDegree` `DFunLike.coe` `LinearMap` `RingHom.id` `module` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent`	—	`ext` `coeff_eq_zero_of_totalDegree_lt` `coeff_sum` `Finset.sum_congr` `coeff_homogeneousComponent` `Finset.sum_ite_eq` `Nat.instNoMaxOrder`
`totalDegree_eq_zero_iff` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`weightedTotalDegree_one` `weightedTotalDegree_eq_zero_iff` `Nat.instCanonicallyOrderedAdd` `nonTorsionWeight_of` `Nat.instIsAddTorsionFree` `one_ne_zero`
`totalDegree_zero_iff_isHomogeneous` 📖	mathematical	—	`totalDegree` `IsHomogeneous`	—	`weightedTotalDegree_one` `isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero` `Nat.instCanonicallyOrderedAdd` `IsHomogeneous.eq_1`
`weightedHomogeneousSubmodule_one` 📖	mathematical	—	`weightedHomogeneousSubmodule` `Nat.instAddCommMonoid` `Pi.instOne` `Nat.instOne` `homogeneousSubmodule`	—	—
`weightedTotalDegree_one` 📖	mathematical	—	`weightedTotalDegree` `Nat.instAddCommMonoid` `Lattice.toSemilatticeSup` `Nat.instLattice` `Nat.instOrderBot` `Pi.instOne` `Nat.instOne` `totalDegree`	—	`mul_one`
`weightedTotalDegree_rename_of_injective` 📖	mathematical	—	`weightedTotalDegree` `Nat.instAddCommMonoid` `Lattice.toSemilatticeSup` `Nat.instLattice` `Nat.instOrderBot` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`support_rename_of_injective` `Finset.sup_image` `Finsupp.linearCombination_mapDomain`

MvPolynomial.HomogeneousSubmodule

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` `Nat.instAddMonoid` `MvPolynomial.homogeneousSubmodule`	—	`MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid`

MvPolynomial.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_mul` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `MvPolynomial.C`	—	`zero_add` `mul` `MvPolynomial.isHomogeneous_C`
`add` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Submodule.add_mem`
`aeval` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval`	—	`eval₂` `MvPolynomial.isHomogeneous_C`
`coeff_eq_zero` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial.coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero` `Finsupp.degree_eq_weight_one`
`coeff_isHomogeneous_of_optionEquivLeft_symm` 📖	mathematical	`MvPolynomial.IsHomogeneous` `DFunLike.coe` `AlgEquiv` `Polynomial` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `MvPolynomial.algebra` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `MvPolynomial.optionEquivLeft`	`Polynomial.coeff`	—	`Finite.exists_equiv_fin` `rename_isHomogeneous` `MvPolynomial.finSuccEquiv_rename_finSuccEquiv` `AlgEquiv.apply_symm_apply` `Polynomial.coeff_map` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `finSuccEquiv_coeff_isHomogeneous` `rename_isHomogeneous_iff` `Equiv.injective`
`eq_zero_of_forall_eval_eq_zero` 📖	mathematical	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`MvPolynomial.instCommRingMvPolynomial`	—	`eq_zero_of_forall_eval_eq_zero_of_le_card` `LE.le.trans` `Cardinal.natCast_le_aleph0` `Cardinal.infinite_iff`
`eq_zero_of_forall_eval_eq_zero_of_le_card` 📖	mathematical	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`MvPolynomial.instCommRingMvPolynomial`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `MvPolynomial.exists_fin_rename` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `rename_isHomogeneous_iff` `Function.factorsThrough_iff` `Nontrivial.to_nonempty` `IsDomain.toNontrivial` `Function.Injective.factorsThrough` `MvPolynomial.eval_rename`
`eval₂` 📖	mathematical	`MvPolynomial.IsHomogeneous` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike`	`MvPolynomial.eval₂`	—	`sum` `zero_add` `mul` `Finset.mul_sum` `Finsupp.mem_support_iff` `Finsupp.weight_apply` `Finset.sum_congr` `mul_one` `prod` `pow`
`finSuccEquiv_coeff_isHomogeneous` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`Polynomial.coeff` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `DFunLike.coe` `AlgEquiv` `Polynomial` `Polynomial.semiring` `MvPolynomial.algebra` `Algebra.id` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `MvPolynomial.finSuccEquiv`	—	`MvPolynomial.finSuccEquiv_coeff_coeff` `mul_one` `Finsupp.sum_cons` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`funext` 📖	—	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	—	`funext_of_le_card` `LE.le.trans` `Cardinal.natCast_le_aleph0` `Cardinal.infinite_iff`
`funext_of_le_card` 📖	—	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	—	`sub_eq_zero` `eq_zero_of_forall_eval_eq_zero_of_le_card` `sub` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`inj_right` 📖	—	`MvPolynomial.IsHomogeneous`	—	—	`MvPolynomial.exists_coeff_ne_zero`
`map` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map`	—	`one_mul` `eval₂` `MvPolynomial.isHomogeneous_C` `MvPolynomial.isHomogeneous_X`
`mul` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`MvPolynomial.homogeneousSubmodule_mul` `Submodule.mul_mem_mul` `IsScalarTower.right`
`neg` 📖	mathematical	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring`	`MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`Submodule.neg_mem`
`of_map` 📖	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `MvPolynomial.IsHomogeneous` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.map`	—	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MvPolynomial.coeff_map`
`pow` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Finset.prod_const` `Finset.card_range` `Finset.sum_const` `mul_comm` `prod`
`prod` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `Finset.sum` `Nat.instAddCommMonoid`	—	`Finset.induction_on` `Finset.prod_insert` `Finset.sum_insert` `mul`
`rename_isHomogeneous` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.rename`	—	`MvPolynomial.support_sum_monomial_coeff` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `MvPolynomial.rename_monomial` `sum` `MvPolynomial.isHomogeneous_monomial` `Finsupp.sum_mapDomain_index_addMonoidHom` `mul_one` `MvPolynomial.mem_support_iff`
`rename_isHomogeneous_iff` 📖	mathematical	—	`MvPolynomial.IsHomogeneous` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.rename`	—	`mul_one` `MvPolynomial.coeff_rename_mapDomain` `rename_isHomogeneous`
`sub` 📖	mathematical	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring`	`MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`Submodule.sub_mem`
`sum` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Submodule.sum_mem`
`totalDegree` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial.totalDegree`	—	`le_antisymm` `totalDegree_le` `MvPolynomial.exists_coeff_ne_zero` `Finset.sum_congr` `Finsupp.mem_support_iff` `mul_one` `Finset.le_sup`
`totalDegree_le` 📖	mathematical	`MvPolynomial.IsHomogeneous`	`MvPolynomial.totalDegree`	—	`Finset.sup_le` `Finset.sum_congr` `MvPolynomial.mem_support_iff` `mul_one`

MvPolynomial.IsHomogeneous.HomogeneousSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gcommSemiring` 📖	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` `Nat.instAddMonoid` `MvPolynomial.homogeneousSubmodule`	—	`MvPolynomial.isHomogeneous_one` `MvPolynomial.IsHomogeneous.mul`

MvPolynomial.decomposition

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.homogeneousSubmodule` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum.Decomposition.decompose'` `Submodule.addSubmonoidClass` `MvPolynomial.decomposition` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `MvPolynomial.homogeneousComponent`	—	`MvPolynomial.weightedDecomposition.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.homogeneousSubmodule` `MvPolynomial.decomposition` `DFunLike.coe` `AddMonoidHom` `DirectSum` `SetLike.instMembership` `Submodule.addCommMonoid` `AddZeroClass.toAddZero` `Pi.addZeroClass` `Set.Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `Finsupp` `AddZero.toZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `MvPolynomial.support` `Set` `Set.instMembership` `instAddCommMonoidDirectSum` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `MvPolynomial.homogeneousComponent` `MvPolynomial.homogeneousComponent_mem`	—	`Submodule.addSubmonoidClass` `MvPolynomial.homogeneousComponent_mem` `Finsupp.degree_eq_weight_one`

---

← Back to Index