Documentation Verification Report

Ideal

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

Statistics

Metric	Count
Definitions `idealOfVars`	1
Theorems `sPolynomial_mem_ideal`, `sPolynomial_mem_sup_ideal`, `span_leadingTerm_eq_span_monomial`, `span_leadingTerm_eq_span_monomial'`, `span_leadingTerm_eq_span_monomial₀`, `span_leadingTerm_insert_zero`, `span_leadingTerm_sdiff_singleton_zero`, `C_mem_pow_idealOfVars_iff`, `idealOfVars_eq_restrictSupportIdeal`, `idealOfVars_fg`, `mem_ideal_span_X_image`, `mem_ideal_span_monomial_image`, `mem_ideal_span_monomial_image_iff_dvd`, `mem_pow_idealOfVars_iff`, `mem_pow_idealOfVars_iff'`, `mk_eq_eval₂`, `mkₐ_eq_aeval`, `monomial_mem_pow_idealOfVars_iff`, `pow_idealOfVars`, `pow_idealOfVars_eq_span`	20
Total	21

MonomialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sPolynomial_mem_ideal` 📖	mathematical	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `sPolynomial`	—	`sub_mem` `Submodule.addSubgroupClass` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Ideal.mul_mem_left`
`sPolynomial_mem_sup_ideal` 📖	mathematical	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `sPolynomial`	—	`sub_mem` `Submodule.addSubgroupClass` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Ideal.mul_mem_left` `Ideal.mem_sup_left` `Ideal.mem_sup_right`
`span_leadingTerm_eq_span_monomial` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `leadingCoeff`	`Ideal.span` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Set.image` `leadingTerm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `degree` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`le_antisymm` `Ideal.span_le` `Set.image_subset_iff` `Set.mem_preimage` `SetLike.mem_coe` `C_mul_leadingCoeff_monomial_degree` `Ideal.mul_mem_left` `Ideal.subset_span` `mul_assoc` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsUnit.val_inv_mul` `MvPolynomial.C_1` `one_mul`
`span_leadingTerm_eq_span_monomial'` 📖	mathematical	—	`Ideal.span` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Set.image` `leadingTerm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `degree` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Set` `Set.instSDiff` `Set.instSingletonSet` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`span_leadingTerm_eq_span_monomial₀`
`span_leadingTerm_eq_span_monomial₀` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `leadingCoeff` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	`Ideal.span` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Set.image` `leadingTerm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `degree` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instSDiff` `Set.instSingletonSet` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`span_leadingTerm_sdiff_singleton_zero` `span_leadingTerm_eq_span_monomial`
`span_leadingTerm_insert_zero` 📖	mathematical	—	`Ideal.span` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Set.image` `leadingTerm` `Set` `Set.instInsert` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`Set.insert_eq_of_mem` `image_leadingTerm_insert_zero` `Ideal.span_insert_zero`
`span_leadingTerm_sdiff_singleton_zero` 📖	mathematical	—	`Ideal.span` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Set.image` `leadingTerm` `Set` `Set.instSDiff` `Set.instSingletonSet` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`Ideal.span_sdiff_singleton_zero` `image_leadingTerm_sdiff_singleton_zero`

MvPolynomial

Definitions

Name	Category	Theorems
`idealOfVars` 📖	CompOp	8 math math: `pow_idealOfVars`, `idealOfVars_eq_restrictSupportIdeal`, `mem_pow_idealOfVars_iff`, `pow_idealOfVars_eq_span`, `mem_pow_idealOfVars_iff'`, `monomial_mem_pow_idealOfVars_iff`, `C_mem_pow_idealOfVars_iff`, `idealOfVars_fg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_mem_pow_idealOfVars_iff` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `idealOfVars` `DFunLike.coe` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`C_0` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `IsScalarTower.right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `Nat.instCanonicallyOrderedAdd` `monomial_mem_pow_idealOfVars_iff`
`idealOfVars_eq_restrictSupportIdeal` 📖	mathematical	—	`idealOfVars` `restrictSupportIdeal` `Set.preimage` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Set.Ici` `PartialOrder.toPreorder` `Nat.instPartialOrder` `IsUpperSet.preimage` `Finsupp.preorder` `Nat.instPreorder` `isUpperSet_Ici` `Finsupp.degree_mono` `Nat.instCanonicallyOrderedAdd`	—	`le_antisymm` `IsUpperSet.preimage` `isUpperSet_Ici` `Finsupp.degree_mono` `Nat.instCanonicallyOrderedAdd` `Finsupp.degree_single` `instReflLe` `IsScalarTower.right` `instIsConcreteLE` `Submodule.restrictScalars_mem` `SetLike.le_def` `restrictSupport_eq_span` `Submodule.span_le` `Set.image_subset_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `le_iff_exists_add'` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `monomial_add_single` `pow_one` `Ideal.mul_mem_left` `Ideal.subset_span`
`idealOfVars_fg` 📖	mathematical	—	`Ideal.FG` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `idealOfVars`	—	`Submodule.fg_span` `Set.finite_range`
`mem_ideal_span_X_image` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set.image` `X` `Set` `Set.instMembership`	—	`mem_ideal_span_monomial_image` `Set.image_image` `Nat.instCanonicallyOrderedAdd`
`mem_ideal_span_monomial_image` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership` `Finsupp.instLE`	—	`AddMonoidAlgebra.mem_ideal_span_of'_image` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `add_comm`
`mem_ideal_span_monomial_image_iff_dvd` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `AddMonoidAlgebra.nonUnitalSemiring` `AddMonoid.toAddSemigroup` `coeff`	—	`mem_ideal_span_monomial_image` `mem_support_iff`
`mem_pow_idealOfVars_iff` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `idealOfVars` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`IsScalarTower.right` `IsUpperSet.preimage` `isUpperSet_Ici` `Finsupp.degree_mono` `Nat.instCanonicallyOrderedAdd` `pow_idealOfVars`
`mem_pow_idealOfVars_iff'` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `idealOfVars` `coeff` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`mk_eq_eval₂` 📖	mathematical	—	`OneHom.toFun` `MvPolynomial` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Ideal.instHasQuotient` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `eval₂` `AddMonoidAlgebra.semiring` `CommSemiring.toSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commSemiring` `algebraMap` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `AddMonoidAlgebra.algebra` `Algebra.id` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `X`	—	`Ideal.instIsTwoSided_1` `mkₐ_eq_aeval` `aeval_X`
`mkₐ_eq_aeval` 📖	mathematical	—	`Ideal.Quotient.mkₐ` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `CommSemiring.toSemiring` `Algebra.id` `Ideal.instIsTwoSided_1` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `aeval` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.commSemiring` `Ideal.Quotient.algebra` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike` `X`	—	`algHom_ext` `Ideal.instIsTwoSided_1` `aeval_X`
`monomial_mem_pow_idealOfVars_iff` 📖	mathematical	—	`MvPolynomial` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `idealOfVars` `DFunLike.coe` `LinearMap` `RingHom.id` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	—
`pow_idealOfVars` 📖	mathematical	—	`Ideal` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `idealOfVars` `restrictSupportIdeal` `Set.preimage` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Set.Ici` `Nat.instPreorder` `IsUpperSet.preimage` `Finsupp.preorder` `isUpperSet_Ici` `Finsupp.degree_mono` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd`	—	`IsScalarTower.right` `IsUpperSet.preimage` `isUpperSet_Ici` `Finsupp.degree_mono` `Nat.instCanonicallyOrderedAdd` `idealOfVars_eq_restrictSupportIdeal` `Submodule.restrictScalars_injective` `Submodule.restrictScalars.congr_simp` `pow_zero` `Ideal.one_eq_top` `Set.Ici_zero_eq_univ` `restrictSupportIdeal.congr_simp` `restrictSupport_univ` `Submodule.restrictScalars_pow` `Set.Ici_nsmul_eq` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_one`
`pow_idealOfVars_eq_span` 📖	mathematical	—	`Ideal` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Algebra.id` `idealOfVars` `Ideal.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.preimage` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Set` `Set.instSingletonSet`	—	`IsScalarTower.right` `idealOfVars.eq_1` `Ideal.span.eq_1` `Submodule.span_pow` `Set.image_univ` `Finsupp.image_pow_eq_finsuppProd_image` `Set.image_congr` `monomial_eq` `one_mul`

---

← Back to Index