Homogenize

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

Statistics

Metric	Count
Definitions `homogenize`, `homogenizeLM`	2
Theorems `aeval_homogenize_X_one`, `aeval_homogenize_of_eq_one`, `coeff_homogenize`, `eval_homogenize`, `eval₂_homogenize_of_eq_one`, `homogenizeLM_apply`, `homogenize_C`, `homogenize_C_mul`, `homogenize_X`, `homogenize_X_pow`, `homogenize_add`, `homogenize_dvd`, `homogenize_eq_of_isHomogeneous`, `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`	25
Total	27

Polynomial

Definitions

Name	Category	Theorems
`homogenize` 📖	CompOp	25 math math: `homogenize_map`, `eval₂_homogenize_of_eq_one`, `homogenize_smul`, `isHomogeneous_homogenize`, `homogenize_eq_of_isHomogeneous`, `aeval_homogenize_X_one`, `homogenize_add`, `eval_homogenize`, `homogenize_X_pow`, `homogenize_finsetSum`, `homogenize_C_mul`, `homogenize_finsetProd`, `homogenize_monomial_of_lt`, `coeff_homogenize`, `homogenize_sub`, `homogenize_zero`, `homogenize_C`, `homogenize_X`, `homogenize_one`, `homogenizeLM_apply`, `homogenize_mul`, `aeval_homogenize_of_eq_one`, `homogenize_dvd`, `homogenize_neg`, `homogenize_monomial`
`homogenizeLM` 📖	CompOp	1 math math: `homogenizeLM_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_homogenize_X_one` 📖	mathematical	`natDegree` `CommSemiring.toSemiring`	`DFunLike.coe` `AlgHom` `MvPolynomial` `Polynomial` `MvPolynomial.commSemiring` `commSemiring` `MvPolynomial.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` `MvPolynomial.commSemiring` `MvPolynomial.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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `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`
`eval_homogenize` 📖	mathematical	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `homogenize` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `eval` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Monoid.toNatPow` `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₂`	—	`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`
`homogenizeLM_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `MvPolynomial.commSemiring` `module` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `homogenizeLM` `homogenize`	—	—
`homogenize_C` 📖	mathematical	—	`homogenize` `DFunLike.coe` `RingHom` `Polynomial` `CommSemiring.toSemiring` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.C`	—	`C_mul'` `homogenize_smul` `MvPolynomial.C_mul'`
`homogenize_X` 📖	mathematical	—	`homogenize` `X` `CommSemiring.toSemiring` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_one` `homogenize_X_pow`
`homogenize_X_pow` 📖	mathematical	—	`homogenize` `Polynomial` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `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` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring`	—	`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` `MvPolynomial.commSemiring` `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` `MvPolynomial.commSemiring` `commSemiring` `MvPolynomial.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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `add_tsub_cancel_left` `Nat.instOrderedSub`
`homogenize_finsetProd` 📖	mathematical	`natDegree` `CommSemiring.toSemiring`	`homogenize` `Finset.prod` `Polynomial` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum` `Nat.instAddCommMonoid` `MvPolynomial` `MvPolynomial.commSemiring`	—	`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` `MvPolynomial.commSemiring`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`homogenize_map` 📖	mathematical	—	`homogenize` `map` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `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` `MvPolynomial.commSemiring` `MvPolynomial.module` `MvPolynomial.monomial` `Finsupp.update` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.single`	—	`homogenize.eq_1` `Finset.sum_eq_single` `coeff_monomial` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `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` `MvPolynomial.commSemiring`	—	`homogenize.eq_1` `Finset.sum_eq_zero` `coeff_monomial` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`homogenize_mul` 📖	mathematical	`natDegree` `CommSemiring.toSemiring`	`homogenize` `Polynomial` `instMul` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring`	—	`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` `Ring.toAddCommGroup` `MvPolynomial.instCommRingMvPolynomial`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`homogenize_one` 📖	mathematical	—	`homogenize` `Polynomial` `CommSemiring.toSemiring` `instOne` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPolynomial.commSemiring` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `MvPolynomial.commSemiring` `MvPolynomial.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` `MvPolynomial.instCommRingMvPolynomial`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`homogenize_zero` 📖	mathematical	—	`homogenize` `Polynomial` `CommSemiring.toSemiring` `instZero` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring`	—	`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`

---

← Back to Index