Homogenize

📁 Source: Mathlib/Algebra/Polynomial/Homogenize.lean

Statistics

Metric	Count
Definitions homogenize, homogenizeLM, toTupleMvPolynomial	3
Theorems aeval_homogenize_X_one, aeval_homogenize_of_eq_one, coeff_homogenize, eq_zero_of_homogenize_eq_zero, eval_X_toTupleMvPolynomial_zero_eq, eval_eq_div_eval_toTupleMvPolynomial, eval_homogenize, eval₂_homogenize_of_eq_one, finsuppSum_homogenize_eq, homogenizeLM_apply, homogenize_C, homogenize_C_mul, homogenize_X, homogenize_X_pow, homogenize_add, homogenize_dvd, homogenize_eq_of_isHomogeneous, homogenize_eq_zero_iff, homogenize_finsetProd, homogenize_finsetSum, homogenize_map, homogenize_monomial, homogenize_monomial_of_lt, homogenize_mul, homogenize_neg, homogenize_one, homogenize_smul, homogenize_sub, homogenize_zero, isHomogeneous_homogenize, isHomogenous_toTupleMvPolynomial, sum_eq_natDegree_of_mem_support_homogenize, toTupleMvPolynomial_one_eq, toTupleMvPolynomial_zero_eq	34
Total	37

Polynomial

Definitions

Name	Category	Theorems
homogenize 📖	CompOp	28 math math: homogenize_map, eval₂_homogenize_of_eq_one, homogenize_smul, isHomogeneous_homogenize, homogenize_eq_of_isHomogeneous, finsuppSum_homogenize_eq, aeval_homogenize_X_one, homogenize_add, eval_homogenize, homogenize_X_pow, toTupleMvPolynomial_zero_eq, homogenize_finsetSum, homogenize_C_mul, homogenize_finsetProd, homogenize_monomial_of_lt, coeff_homogenize, homogenize_sub, homogenize_zero, homogenize_C, homogenize_X, homogenize_eq_zero_iff, homogenize_one, homogenizeLM_apply, homogenize_mul, aeval_homogenize_of_eq_one, homogenize_dvd, homogenize_neg, homogenize_monomial
homogenizeLM 📖	CompOp	1 math math: homogenizeLM_apply
toTupleMvPolynomial 📖	CompOp	5 math math: eval_eq_div_eval_toTupleMvPolynomial, toTupleMvPolynomial_one_eq, toTupleMvPolynomial_zero_eq, eval_X_toTupleMvPolynomial_zero_eq, isHomogenous_toTupleMvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_homogenize_X_one 📖	mathematical	natDegree CommSemiring.toSemiring	DFunLike.coe AlgHom MvPolynomial Polynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid commSemiring AddMonoidAlgebra.algebra Algebra.id algebraOfAlgebra AlgHom.funLike MvPolynomial.aeval Matrix.vecCons X instOne Matrix.vecEmpty homogenize	—	aeval_homogenize_of_eq_one Matrix.cons_val_fin_one aeval_X_left
aeval_homogenize_of_eq_one 📖	mathematical	natDegree CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval homogenize Polynomial semiring algebraOfAlgebra aeval	—	eval₂_homogenize_of_eq_one
coeff_homogenize 📖	mathematical	—	MvPolynomial.coeff homogenize DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike coeff CommSemiring.toSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	induction_on' homogenize_add MvPolynomial.coeff_add ite_add_ite add_zero coeff_add le_or_gt homogenize_monomial coeff_monomial MvPolynomial.coeff_monomial Finsupp.ext Fintype.complete Finsupp.coe_update Function.update_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Finsupp.single_eq_same Function.update_self add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd homogenize_monomial_of_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
eq_zero_of_homogenize_eq_zero 📖	mathematical	natDegree CommSemiring.toSemiring homogenize MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	Polynomial CommSemiring.toSemiring instZero	—	ext le_or_gt coeff_homogenize Finsupp.coe_update Function.update_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Finsupp.single_eq_same Function.update_self LE.le.trans coeff_eq_zero_of_natDegree_lt
eval_X_toTupleMvPolynomial_zero_eq 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial Polynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid commSemiring AddMonoidAlgebra.algebra Algebra.id algebraOfAlgebra AlgHom.funLike MvPolynomial.aeval Matrix.vecCons X instOne Matrix.vecEmpty toTupleMvPolynomial instMul	—	aeval_homogenize_X_one instReflLe Matrix.cons_val_fin_one map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MvPolynomial.aeval_X one_pow mul_one
eval_eq_div_eval_toTupleMvPolynomial 📖	mathematical	—	eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty toTupleMvPolynomial	—	eval_homogenize instReflLe Matrix.cons_val_fin_one NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing div_one one_pow mul_one map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MvPolynomial.eval_X
eval_homogenize 📖	mathematical	natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring	DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval homogenize Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring eval DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finset.sum_congr MvPolynomial.eval_sum eval_eq_sum_range' Finset.sum_mul MvPolynomial.eval_monomial Finsupp.update_eq_add_single Finsupp.single_eq_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Finsupp.prod_add_index' pow_zero pow_add Finsupp.prod_single_index pow_sub₀ Nat.instNoMaxOrder Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf
eval₂_homogenize_of_eq_one 📖	mathematical	natDegree CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	MvPolynomial.eval₂ homogenize eval₂ CommSemiring.toSemiring	—	induction_with_natDegree_le homogenize_zero MvPolynomial.eval₂_zero eval₂_zero homogenize_C_mul homogenize_X_pow MvPolynomial.eval₂_mul MvPolynomial.eval₂_C MvPolynomial.eval₂_pow MvPolynomial.eval₂_X one_pow mul_one eval₂_mul eval₂_C eval₂_X_pow homogenize_add MvPolynomial.eval₂_add eval₂_add
finsuppSum_homogenize_eq 📖	mathematical	—	Finsupp.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring homogenize natDegree sum	—	MvPolynomial.sum_def sum_def Finset.sum_nbij' coeff_homogenize sum_eq_natDegree_of_mem_support_homogenize Finsupp.coe_update Function.update_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Finsupp.single_eq_same Function.update_self mem_support_iff le_natDegree_of_mem_supp
homogenizeLM_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass module Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike homogenizeLM homogenize	—	—
homogenize_C 📖	mathematical	—	homogenize DFunLike.coe RingHom Polynomial CommSemiring.toSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass MvPolynomial.C Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp.instAddMonoid MvPolynomial.X	—	MvPolynomial.C_mul_X_pow_eq_monomial Finsupp.single_zero tsub_zero Nat.instOrderedSub homogenize_monomial
homogenize_C_mul 📖	mathematical	—	homogenize Polynomial CommSemiring.toSemiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass MvPolynomial.C	—	C_mul' homogenize_smul MvPolynomial.C_mul'
homogenize_X 📖	mathematical	—	homogenize X CommSemiring.toSemiring MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.X Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp.instAddMonoid	—	pow_one homogenize_X_pow
homogenize_X_pow 📖	mathematical	—	homogenize Polynomial CommSemiring.toSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.semiring Finsupp.instAddMonoid MvPolynomial.X	—	X_pow_eq_monomial homogenize_monomial Finsupp.update_eq_add_single Finsupp.single_eq_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 MvPolynomial.monomial_single_add MvPolynomial.X_pow_eq_monomial
homogenize_add 📖	mathematical	—	homogenize Polynomial CommSemiring.toSemiring instAdd MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	Finset.sum_congr coeff_add map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Finset.sum_add_distrib
homogenize_dvd 📖	mathematical	Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid homogenize natDegree	—	homogenize_zero MulZeroClass.zero_mul MulZeroClass.mul_zero natDegree_mul homogenize_mul le_rfl dvd_mul_right
homogenize_eq_of_isHomogeneous 📖	mathematical	MvPolynomial.IsHomogeneous DFunLike.coe AlgHom MvPolynomial Polynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid commSemiring AddMonoidAlgebra.algebra Algebra.id algebraOfAlgebra AlgHom.funLike MvPolynomial.aeval Matrix.vecCons X instOne Matrix.vecEmpty	homogenize	—	MvPolynomial.as_sum MvPolynomial.aeval_sum Finset.sum_congr MvPolynomial.aeval_monomial homogenize_finsetSum homogenize_C_mul MvPolynomial.monomial_eq Finsupp.prod_fintype pow_zero Fin.prod_univ_two Matrix.cons_val_fin_one one_pow mul_one Finsupp.sum_fintype Fin.sum_univ_two homogenize_X_pow IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd add_tsub_cancel_left Nat.instOrderedSub
homogenize_eq_zero_iff 📖	mathematical	natDegree CommSemiring.toSemiring	homogenize MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Polynomial instZero	—	eq_zero_of_homogenize_eq_zero homogenize_zero
homogenize_finsetProd 📖	mathematical	natDegree CommSemiring.toSemiring	homogenize Finset.prod Polynomial CommSemiring.toSemiring CommSemiring.toCommMonoid commSemiring Finset.sum Nat.instAddCommMonoid MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid	—	Finset.cons_induction homogenize_one pow_zero Finset.prod_cons Finset.sum_cons homogenize_mul LE.le.trans natDegree_prod_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
homogenize_finsetSum 📖	mathematical	—	homogenize Finset.sum Polynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring MvPolynomial AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
homogenize_map 📖	mathematical	—	homogenize map CommSemiring.toSemiring DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map	—	Finset.sum_congr coeff_map map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.map_monomial
homogenize_monomial 📖	mathematical	—	homogenize DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial MvPolynomial AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddMonoidAlgebra.module MvPolynomial.monomial Finsupp.update Finsupp.single	—	homogenize.eq_1 Finset.sum_eq_single coeff_monomial add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd coeff_monomial_same instIsEmptyFalse
homogenize_monomial_of_lt 📖	mathematical	—	homogenize DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	homogenize.eq_1 Finset.sum_eq_zero coeff_monomial IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
homogenize_mul 📖	mathematical	natDegree CommSemiring.toSemiring	homogenize Polynomial CommSemiring.toSemiring instMul MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	homogenize_eq_of_isHomogeneous MvPolynomial.IsHomogeneous.mul isHomogeneous_homogenize map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass aeval_homogenize_X_one
homogenize_neg 📖	mathematical	—	homogenize CommRing.toCommSemiring Polynomial CommSemiring.toSemiring instNeg CommRing.toRing MvPolynomial NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddMonoidAlgebra.addAddCommGroup Finsupp MulZeroClass.toZero Nat.instMulZeroClass	—	map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
homogenize_one 📖	mathematical	—	homogenize Polynomial CommSemiring.toSemiring instOne MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid MvPolynomial.X	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul homogenize_C
homogenize_smul 📖	mathematical	—	homogenize Polynomial CommSemiring.toSemiring SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPolynomial AddZero.toZero AddMonoidAlgebra Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddCommMonoid.toAddMonoid AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.smulZeroClass	—	Finset.sum_congr coeff_smul Finset.smul_sum MvPolynomial.smul_monomial
homogenize_sub 📖	mathematical	—	homogenize CommRing.toCommSemiring Polynomial CommSemiring.toSemiring instSub CommRing.toRing MvPolynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
homogenize_zero 📖	mathematical	—	homogenize Polynomial CommSemiring.toSemiring instZero MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	Finset.sum_congr MvPolynomial.monomial_zero Finset.sum_const_zero
isHomogeneous_homogenize 📖	mathematical	—	MvPolynomial.IsHomogeneous homogenize	—	MvPolynomial.IsHomogeneous.sum MvPolynomial.isHomogeneous_monomial Finsupp.update_eq_add_single Finsupp.single_eq_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Finsupp.degree_single
isHomogenous_toTupleMvPolynomial 📖	mathematical	—	MvPolynomial.IsHomogeneous toTupleMvPolynomial natDegree CommSemiring.toSemiring	—	Fintype.complete Matrix.cons_val_fin_one MvPolynomial.isHomogeneous_X_pow
sum_eq_natDegree_of_mem_support_homogenize 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike MvPolynomial.support homogenize natDegree CommSemiring.toSemiring	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike natDegree CommSemiring.toSemiring	—	MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support isHomogeneous_homogenize Finsupp.degree_eq_sum Fin.sum_univ_two
toTupleMvPolynomial_one_eq 📖	mathematical	—	toTupleMvPolynomial MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid MvPolynomial.X natDegree	—	—
toTupleMvPolynomial_zero_eq 📖	mathematical	—	toTupleMvPolynomial homogenize natDegree CommSemiring.toSemiring	—	—

---

← Back to Index