CommRing

📁 Source: Mathlib/Algebra/MvPolynomial/CommRing.lean

Statistics

Metric	Count
Definitions `CommRing`, `homEquiv`	2
Theorems `C_neg`, `C_sub`, `coeff_neg`, `coeff_sub`, `degreeOf_neg`, `degreeOf_sub_le`, `degreeOf_sub_lt`, `degrees_neg`, `degrees_sub_le`, `eval_neg`, `eval_sub`, `eval₂Hom_X`, `eval₂_neg`, `eval₂_sub`, `hom_C`, `support_neg`, `support_sub`, `totalDegree_neg`, `totalDegree_sub`, `totalDegree_sub_C_le`, `vars_neg`, `vars_sub_of_disjoint`, `vars_sub_subset`	23
Total	25

MvPolynomial

Definitions

Name	Category	Theorems
`homEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_neg` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `RingHom.instFunLike` `C` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidAlgebra.addAddCommGroup`	—	`map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`C_sub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `RingHom.instFunLike` `C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidAlgebra.ring` `Finsupp.instAddMonoid`	—	`map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`coeff_neg` 📖	mathematical	—	`coeff` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Ring.toAddCommGroup`	—	`Finsupp.neg_apply`
`coeff_sub` 📖	mathematical	—	`coeff` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`Finsupp.sub_apply`
`degreeOf_neg` 📖	mathematical	—	`degreeOf` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing`	—	`degreeOf.eq_1` `degrees_neg`
`degreeOf_sub_le` 📖	mathematical	—	`degreeOf` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`sub_eq_add_neg` `degreeOf_neg` `degreeOf_add_le`
`degreeOf_sub_lt` 📖	mathematical	`coeff` `CommRing.toCommSemiring`	`degreeOf` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`degreeOf_lt_iff`
`degrees_neg` 📖	mathematical	—	`degrees` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing`	—	`degrees.eq_1` `support_neg`
`degrees_sub_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Multiset.instUnion`	—	`degrees_def` `coeff_sub` `AddMonoidAlgebra.supDegree_sub_le`
`eval_neg` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `CommRing.toRing` `Ring.toAddCommGroup`	—	`eval₂_neg`
`eval_sub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `CommRing.toRing` `Finsupp.instAddMonoid`	—	`eval₂_sub`
`eval₂Hom_X` 📖	mathematical	—	`eval₂` `Int.instCommSemiring` `CommRing.toCommSemiring` `MvPolynomial` `DFunLike.coe` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `X`	—	`induction_on` `hom_C` `eval₂_C` `eq_intCast` `RingHom.instRingHomClass` `eval₂_add` `RingHom.map_add` `eval₂_mul` `eval₂_X` `RingHom.map_mul`
`eval₂_neg` 📖	mathematical	—	`eval₂` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Ring.toAddCommGroup`	—	`RingHom.map_neg`
`eval₂_sub` 📖	mathematical	—	`eval₂` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`RingHom.map_sub`
`hom_C` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `C` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`eq_intCast` `RingHom.instRingHomClass`
`support_neg` 📖	mathematical	—	`support` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing`	—	`Finsupp.support_neg`
`support_sub` 📖	mathematical	—	`Finset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset.instHasSubset` `support` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Finset.instUnion` `Finsupp.instDecidableEq`	—	`Finsupp.support_sub`
`totalDegree_neg` 📖	mathematical	—	`totalDegree` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing`	—	`support_neg`
`totalDegree_sub` 📖	mathematical	—	`totalDegree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`sub_eq_add_neg` `totalDegree_add` `totalDegree_neg`
`totalDegree_sub_C_le` 📖	mathematical	—	`totalDegree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C`	—	`LE.le.trans_eq` `totalDegree_sub` `totalDegree_C`
`vars_neg` 📖	mathematical	—	`vars` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing`	—	`degrees_neg`
`vars_sub_of_disjoint` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `vars` `CommRing.toCommSemiring`	`vars` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Finset` `Finset.instUnion`	—	`sub_eq_add_neg` `vars_neg` `vars_add_of_disjoint`
`vars_sub_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `vars` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Finset.instUnion`	—	`sub_eq_add_neg` `vars_neg` `vars_add_subset`

(root)

Definitions

Name	Category	Theorems
`CommRing` 📖	CompData	14 math math: `PrimeSpectrum.exists_range_eq_of_isConstructible`, `CommRing.toRing_injective`, `Module.Finite.exists_free_surjective`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq`, `Algebra.Smooth.exists_subalgebra_finiteType`, `Algebra.Etale.exists_subalgebra_fg`, `Algebra.Smooth.exists_finiteType`, `nonempty_commRing_iff`, `Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux`, `nonempty_commRing`, `Polynomial.Monic.exists_splits_map`, `Algebra.Smooth.exists_subalgebra_fg`, `Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg`

---

← Back to Index