Basic

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

Statistics

Metric	Count
Definitions `basisMonomials`, `basisRestrictSupport`, `restrictDegree`, `restrictSupport`, `restrictSupportIdeal`, `restrictTotalDegree`	6
Theorems `coe_basisMonomials`, `instCharP`, `instCharZero`, `instExpChar`, `instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite`, `instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite`, `instFree`, `instSmall`, `linearIndependent_X`, `mapRange_eq_map`, `mem_restrictDegree`, `mem_restrictDegree_iff_sup`, `mem_restrictSupport_iff`, `mem_restrictTotalDegree`, `monomial_mem_restrictSupport`, `restrictScalars_restrictSupportIdeal`, `restrictSupport_add`, `restrictSupport_eq_span`, `restrictSupport_mono`, `restrictSupport_nsmul`, `restrictSupport_univ`, `restrictSupport_zero`, `restrictTotalDegree_le_restrictDegree`	23
Total	29

MvPolynomial

Definitions

Name	Category	Theorems
`basisMonomials` 📖	CompOp	2 math math: `coe_basisMonomials`, `Module.Basis.symmetricAlgebra_repr_apply`
`basisRestrictSupport` 📖	CompOp	—
`restrictDegree` 📖	CompOp	6 math math: `map_restrict_dom_evalₗ`, `mem_restrictDegree`, `indicator_mem_restrictDegree`, `instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite`, `mem_restrictDegree_iff_sup`, `restrictTotalDegree_le_restrictDegree`
`restrictSupport` 📖	CompOp	9 math math: `restrictSupport_univ`, `restrictSupport_mono`, `restrictSupport_zero`, `restrictScalars_restrictSupportIdeal`, `mem_restrictSupport_iff`, `restrictSupport_nsmul`, `monomial_mem_restrictSupport`, `restrictSupport_add`, `restrictSupport_eq_span`
`restrictSupportIdeal` 📖	CompOp	3 math math: `pow_idealOfVars`, `idealOfVars_eq_restrictSupportIdeal`, `restrictScalars_restrictSupportIdeal`
`restrictTotalDegree` 📖	CompOp	3 math math: `instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite`, `mem_restrictTotalDegree`, `restrictTotalDegree_le_restrictDegree`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_basisMonomials` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Module.Basis.instFunLike` `basisMonomials` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`instCharP` 📖	mathematical	—	`CharP` `MvPolynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`C_eq_coe_nat` `C_0` `CharP.cast_eq_zero_iff`
`instCharZero` 📖	mathematical	—	`CharZero` `MvPolynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`C_eq_coe_nat`
`instExpChar` 📖	mathematical	—	`ExpChar` `MvPolynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`instCharZero` `instCharP`
`instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite` 📖	mathematical	—	`Module.Finite` `MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictDegree` `Submodule.addCommMonoid` `Submodule.module`	—	`Module.Finite.of_basis`
`instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite` 📖	mathematical	—	`Module.Finite` `MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictTotalDegree` `Submodule.addCommMonoid` `Submodule.module`	—	`Set.finite_coe_iff` `Set.Finite.subset` `eq_or_ne` `Eq.trans_le` `LE.le.trans` `Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.mem_support_iff` `Module.Finite.of_basis`
`instFree` 📖	mathematical	—	`Module.Free` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule`	—	`Module.Free.of_basis`
`instSmall` 📖	mathematical	—	`Small` `MvPolynomial`	—	`Finsupp.small` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`linearIndependent_X` 📖	mathematical	—	`LinearIndependent` `MvPolynomial` `X` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule`	—	`LinearIndependent.comp` `Module.Basis.linearIndependent` `Finsupp.single_left_injective` `one_ne_zero`
`mapRange_eq_map` 📖	mathematical	—	`Finsupp.mapRange` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `RingHom.map_zero` `MvPolynomial` `commSemiring` `map`	—	`RingHom.map_zero` `as_sum` `map_zero` `AddMonoidHomClass.toZeroHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finsupp.mapRange_finset_sum` `map_sum` `Finset.sum_congr` `map_monomial` `single_eq_monomial` `Finsupp.mapRange_single`
`mem_restrictDegree` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictDegree` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`restrictDegree.eq_1` `restrictSupport.eq_1` `Finsupp.mem_supported`
`mem_restrictDegree_iff_sup` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictDegree` `Multiset.count` `degrees`	—	`Multiset.count.congr_simp` `degrees_def` `Multiset.count_finset_sup` `Finsupp.count_toMultiset`
`mem_restrictSupport_iff` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictSupport` `Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	—
`mem_restrictTotalDegree` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictTotalDegree` `totalDegree`	—	`totalDegree.eq_1` `Finset.sup_le_iff`
`monomial_mem_restrictSupport` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictSupport` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set` `Set.instMembership` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`monomial_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `support_monomial` `Finset.coe_singleton`
`restrictScalars_restrictSupportIdeal` 📖	mathematical	`IsUpperSet` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLE`	`Submodule.restrictScalars` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `module` `Semiring.toModule` `Algebra.toSMul` `algebra` `Algebra.id` `IsScalarTower.right` `restrictSupportIdeal` `restrictSupport`	—	`IsScalarTower.right`
`restrictSupport_add` 📖	mathematical	—	`restrictSupport` `Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.add` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.mul` `IsScalarTower.right` `algebra` `Algebra.id`	—	`le_antisymm` `IsScalarTower.right` `restrictSupport_eq_span` `Submodule.span_le` `Set.image_subset_iff` `Set.add_subset_iff` `monomial_mul` `mul_one` `Submodule.span_mul_span` `Set.mul_subset_iff`
`restrictSupport_eq_span` 📖	mathematical	—	`restrictSupport` `Submodule.span` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Set.image` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finsupp.supported_eq_span_single`
`restrictSupport_mono` 📖	mathematical	`Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.instHasSubset`	`Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `restrictSupport`	—	`Finsupp.supported_mono`
`restrictSupport_nsmul` 📖	mathematical	—	`restrictSupport` `Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.NSMul` `Finsupp.instZero` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `algebra` `Algebra.id`	—	`IsScalarTower.right` `zero_nsmul` `restrictSupport_zero` `pow_zero` `add_smul` `one_smul` `restrictSupport_add` `pow_succ`
`restrictSupport_univ` 📖	mathematical	—	`restrictSupport` `Set.univ` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Top.top` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.instTop`	—	`Submodule.ext`
`restrictSupport_zero` 📖	mathematical	—	`restrictSupport` `Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.zero` `Finsupp.instZero` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.one`	—	`le_antisymm` `restrictSupport_eq_span` `Submodule.span_le` `Set.image_subset_iff` `coeff_smul` `coeff_one` `mul_ite` `mul_one` `MulZeroClass.mul_zero`
`restrictTotalDegree_le_restrictDegree` 📖	mathematical	—	`Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `restrictTotalDegree` `restrictDegree`	—	`mem_restrictDegree` `LE.le.trans` `degreeOf_le_iff` `degreeOf_le_totalDegree` `mem_restrictTotalDegree`

---

← Back to Index