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`, `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'`, `monomial_mem_pow_idealOfVars_iff`, `pow_idealOfVars`, `pow_idealOfVars_eq_span`	17
Total	18

MonomialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sPolynomial_mem_ideal` 📖	mathematical	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `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` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `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` `MvPolynomial.commSemiring` `Set.image` `leadingTerm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `MvPolynomial.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` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Set.image` `leadingTerm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `degree` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Set` `Set.instSDiff` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Field.toCommRing`	—	`span_leadingTerm_eq_span_monomial₀`
`span_leadingTerm_eq_span_monomial₀` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `leadingCoeff` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring`	`Ideal.span` `Set.image` `leadingTerm` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `degree` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`span_leadingTerm_sdiff_singleton_zero` `span_leadingTerm_eq_span_monomial`
`span_leadingTerm_insert_zero` 📖	mathematical	—	`Ideal.span` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Set.image` `leadingTerm` `Set` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Set.insert_eq_of_mem` `image_leadingTerm_insert_zero` `Ideal.span_insert_zero`
`span_leadingTerm_sdiff_singleton_zero` 📖	mathematical	—	`Ideal.span` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Set.image` `leadingTerm` `Set` `Set.instSDiff` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Ideal.span_sdiff_singleton_zero` `image_leadingTerm_sdiff_singleton_zero`

MvPolynomial

Definitions

Name	Category	Theorems
`idealOfVars` 📖	CompOp	7 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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_mem_pow_idealOfVars_iff` 📖	mathematical	—	`MvPolynomial` `Ideal` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `idealOfVars` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `MulZeroClass.toZero` `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` `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`
`mem_ideal_span_X_image` 📖	mathematical	—	`MvPolynomial` `Ideal` `CommSemiring.toSemiring` `commSemiring` `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` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set.image` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `LinearMap` `RingHom.id` `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` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set.image` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `LinearMap` `RingHom.id` `module` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `coeff`	—	`mem_ideal_span_monomial_image` `mem_support_iff`
`mem_pow_idealOfVars_iff` 📖	mathematical	—	`MvPolynomial` `Ideal` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `idealOfVars` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `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` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `idealOfVars` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`monomial_mem_pow_idealOfVars_iff` 📖	mathematical	—	`MvPolynomial` `Ideal` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `idealOfVars` `DFunLike.coe` `LinearMap` `RingHom.id` `module` `LinearMap.instFunLike` `monomial` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	—
`pow_idealOfVars` 📖	mathematical	—	`Ideal` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `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` `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` `CommSemiring.toSemiring` `commSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `idealOfVars` `Ideal.span` `Set.image` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.preimage` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Set` `Set.instSingletonSet`	—	`IsScalarTower.right` `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