Documentation Verification Report

Homogeneous

πŸ“ Source: Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Statistics

MetricCount
DefinitionsIsHomogeneous, decomposition, gradedAlgebra, homogeneousComponent, homogeneousSubmodule
5
Theoremsmem_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
Total68

Ideal

Theorems

NameKindAssumesProvesValidatesDepends 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

NameCategoryTheorems
IsHomogeneous πŸ“–MathDef
21 mathmath: 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 mathmath: decomposition.decompose'_apply, decomposition.decompose'_eq
gradedAlgebra πŸ“–CompOpβ€”
homogeneousComponent πŸ“–CompOp
12 mathmath: 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 mathmath: 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

NameKindAssumesProvesValidatesDepends 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 πŸ“–mathematicaltotalDegreeDFunLike.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 πŸ“–mathematicalMvPolynomial
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 πŸ“–mathematicalDFunLike.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 πŸ“–mathematicaltotalDegreeIsHomogeneousβ€”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

NameKindAssumesProvesValidatesDepends 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

NameKindAssumesProvesValidatesDepends On
C_mul πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial
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 πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
MvPolynomial.commSemiring
β€”Submodule.add_mem
aeval πŸ“–mathematicalMvPolynomial.IsHomogeneousDFunLike.coe
AlgHom
MvPolynomial
CommSemiring.toSemiring
MvPolynomial.commSemiring
MvPolynomial.algebra
Algebra.id
AlgHom.funLike
MvPolynomial.aeval
β€”evalβ‚‚
MvPolynomial.isHomogeneous_C
coeff_eq_zero πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial.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 πŸ“–mathematicalMvPolynomial.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 πŸ“–mathematicalMvPolynomial.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 πŸ“–mathematicalMvPolynomial.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β‚‚ πŸ“–mathematicalMvPolynomial.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 πŸ“–mathematicalMvPolynomial.IsHomogeneousPolynomial.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 πŸ“–mathematicalMvPolynomial.IsHomogeneousDFunLike.coe
RingHom
MvPolynomial
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
MvPolynomial.commSemiring
RingHom.instFunLike
MvPolynomial.map
β€”one_mul
evalβ‚‚
MvPolynomial.isHomogeneous_C
MvPolynomial.isHomogeneous_X
mul πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial
Distrib.toMul
NonUnitalNonAssocSemiring.toDistrib
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
MvPolynomial.commSemiring
β€”MvPolynomial.homogeneousSubmodule_mul
Submodule.mul_mem_mul
IsScalarTower.right
neg πŸ“–mathematicalMvPolynomial.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 πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial
Monoid.toNatPow
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
CommSemiring.toSemiring
MvPolynomial.commSemiring
β€”Finset.prod_const
Finset.card_range
Finset.sum_const
mul_comm
prod
prod πŸ“–mathematicalMvPolynomial.IsHomogeneousFinset.prod
MvPolynomial
CommSemiring.toCommMonoid
MvPolynomial.commSemiring
Finset.sum
Nat.instAddCommMonoid
β€”Finset.induction_on
Finset.prod_insert
Finset.sum_insert
mul
rename_isHomogeneous πŸ“–mathematicalMvPolynomial.IsHomogeneousDFunLike.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 πŸ“–mathematicalMvPolynomial.IsHomogeneous
CommRing.toCommSemiring
MvPolynomial
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddGroupWithOne.toAddGroup
Ring.toAddGroupWithOne
CommRing.toRing
MvPolynomial.instCommRingMvPolynomial
β€”Submodule.sub_mem
sum πŸ“–mathematicalMvPolynomial.IsHomogeneousFinset.sum
MvPolynomial
NonUnitalNonAssocSemiring.toAddCommMonoid
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
MvPolynomial.commSemiring
β€”Submodule.sum_mem
totalDegree πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial.totalDegreeβ€”le_antisymm
totalDegree_le
MvPolynomial.exists_coeff_ne_zero
Finset.sum_congr
Finsupp.mem_support_iff
mul_one
Finset.le_sup
totalDegree_le πŸ“–mathematicalMvPolynomial.IsHomogeneousMvPolynomial.totalDegreeβ€”Finset.sup_le
Finset.sum_congr
MvPolynomial.mem_support_iff
mul_one

MvPolynomial.IsHomogeneous.HomogeneousSubmodule

Theorems

NameKindAssumesProvesValidatesDepends 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

NameKindAssumesProvesValidatesDepends 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