CommRing

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

Statistics

Metric	Count
Definitions `CommRing`, `homEquiv`, `instCommRingMvPolynomial`	3
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	26

MvPolynomial

Definitions

Name	Category	Theorems
`homEquiv` 📖	CompOp	—
`instCommRingMvPolynomial` 📖	CompOp	283 math math: `AlgebraicGeometry.AffineSpace.map_Spec_map`, `dvd_monomial_one_iff_exists`, `KaehlerDifferential.mvPolynomialBasis_apply`, `coeff_neg`, `MonomialOrder.sPolynomial_leadingTerm_mul'`, `degrees_neg`, `Algebra.PreSubmersivePresentation.jacobiMatrix_naive`, `isJacobsonRing`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc`, `CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd`, `MonomialOrder.monic_X_sub_C`, `AlgebraicIndependent.of_aeval`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv`, `Algebra.Generators.H1Cotangent.δAux_mul`, `Algebra.Presentation.naive_toGenerators`, `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `universalFactorizationMap_comp_map`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_map`, `Algebra.Generators.cotangentSpaceBasis_apply`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `instIsReduced`, `AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop`, `KaehlerDifferential.mvPolynomialBasis_repr_D_X`, `Algebra.Generators.toAlgHom_ofComp_localizationAway`, `Algebra.Presentation.localizationAway_relation`, `StandardEtalePresentation.toPresentation_algebra_smul`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C`, `vars_sub_of_disjoint`, `exists_dvd_map_of_isAlgebraic`, `irreducible_mul_X_add`, `MonomialOrder.degree_sub_le`, `WittVector.mul_polyOfInterest_aux2`, `Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp`, `Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs`, `sum_antidiagonal_card_esymm_psum_eq_zero`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_relation`, `MonomialOrder.div_single`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_σ'`, `Algebra.Presentation.quotientEquiv_symm`, `Algebra.Generators.H1Cotangent.δAux_C`, `Algebra.Generators.naive_val`, `instIsIntegralMvPolynomial`, `Algebra.Generators.compLocalizationAwayAlgHom_X_inl`, `WeierstrassCurve.Jacobian.polynomialY_eq`, `MonomialOrder.sPolynomial_self`, `Algebra.Presentation.naive_relation`, `transcendental_polynomial_aeval_X_iff`, `eval₂_neg`, `Algebra.SubmersivePresentation.ofSubsingleton_relation`, `StandardEtalePair.equivMvPolynomialQuotient_symm_apply`, `Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial`, `xInTermsOfW_eq`, `eq_zero_of_eval_eq_zero`, `transcendental_supported_X_iff`, `algebraicIndependent_polynomial_aeval_X`, `MonomialOrder.degree_neg`, `Algebra.SubmersivePresentation.jacobianRelations_spec`, `LinearMap.toMvPolynomial_add`, `WeierstrassCurve.Projective.polynomialZ_eq`, `TensorProduct.toIntegralClosure_mvPolynomial_bijective`, `IsHomogeneous.sub`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply`, `quotient_map_C_eq_zero`, `AlgebraicClosure.instIsAlgClosureOfIsAlgebraic`, `Algebra.Generators.H1Cotangent.δAux_monomial`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `MonomialOrder.monic_X_add_C`, `vars_sub_subset`, `AlgebraicIndependent.lift_reprField`, `wittPolynomial_one`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `IsLocalization.Away.mvPolynomialQuotientEquiv_apply`, `Algebra.Presentation.naive_relation_apply`, `LinearMap.toMvPolynomial_zero`, `WittVector.mul_polyOfInterest_aux4`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `Algebra.Generators.localizationAway_σ`, `finitePresentation_universalFactorizationMap`, `eval_neg`, `Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom`, `dvd_monomial_iff_exists`, `X_dvd_mul_iff`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord`, `Algebra.PreSubmersivePresentation.naive_toPresentation`, `MonomialOrder.span_leadingTerm_eq_span_monomial'`, `WittVector.bind₁_wittMulN_wittPolynomial`, `dvd_X_mul_iff`, `MonomialOrder.degree_X_sub_C`, `xInTermsOfW_aux`, `irreducible_sumSMulX`, `degreeOf_sub_le`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc`, `vars_neg`, `combinatorial_nullstellensatz_exists_linearCombination`, `finite_universalFactorizationMap`, `wittStructureRat_rec`, `WittVector.mul_polyOfInterest_vars`, `coeff_sumSMulX`, `algebraicIndependent_iff`, `universalFactorizationMapPresentation_map`, `totalDegree_neg`, `AlgebraicClosure.instIsAlgClosure`, `support_neg`, `CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly`, `MonomialOrder.sPolynomial_def`, `MonomialOrder.sPolynomial_antisymm`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none`, `exists_integral_inj_algHom_of_quotient`, `isNilpotent_iff`, `exists_finite_inj_algHom_of_fg`, `degrees_sub_le`, `MonomialOrder.sPolynomial_left_zero`, `wittStructureRat_rec_aux`, `Algebra.Generators.ker_localizationAway`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors`, `dvd_smul_X_iff_exists`, `Algebra.Generators.comp_localizationAway_ker`, `mul_esymm_eq_sum`, `universalFactorizationMapPresentation_relation`, `MonomialOrder.sPolynomial_right_zero`, `WeierstrassCurve.Projective.polynomialX_eq`, `eval₂_sub`, `AlgebraicIndependent.eq_zero_of_aeval_eq_zero`, `WeierstrassCurve.Projective.polynomialY_eq`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul`, `universalFactorizationMapPresentation_algebra_algebraMap`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `WittVector.frobeniusPolyAux_eq`, `Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul`, `AlgebraicGeometry.AffineSpace.map_SpecMap`, `Algebra.Generators.cMulXSubOneCotangent_eq`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc`, `Algebra.Generators.toKaehler_tmul_D`, `quotient_mk_comp_C_isIntegral_of_isJacobsonRing`, `AlgebraicIndependent.liftAlgHom_comp_reprField`, `Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs`, `WeierstrassCurve.Jacobian.polynomialZ_eq`, `MonomialOrder.sPolynomial_monomial_mul`, `RingHom.IsStandardSmooth.exists_etale_mvPolynomial`, `ker_eval₂Hom_universalFactorizationMap`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply`, `WittVector.mul_polyOfInterest_aux1`, `quotientEquivQuotientMvPolynomial_leftInverse`, `quotient_mk_comp_C_injective`, `MonomialOrder.leadingCoeff_neg`, `AlgebraicClosure.Monics.map_eq_prod`, `finrank_eq_zero`, `dvd_monomial_mul_iff_exists`, `Algebra.Generators.H1Cotangent.δAux_X`, `MonomialOrder.div_set`, `dvd_X_iff_exists`, `eval_sub`, `totalDegree_sub`, `StandardEtalePresentation.toPresentation_σ'`, `isIntegral_iff_isIntegral_coeff`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite`, `IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card`, `coeff_sub`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop`, `Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one`, `algebraicIndependent_subtype`, `algebraicIndependent_X`, `Algebra.Presentation.algebraTensorAlgEquiv_symm_relation`, `AlgebraicIndependent.aevalEquivField_apply_coe`, `IsTranscendenceBasis.mvPolynomial`, `transcendental_polynomial_aeval_X`, `WittVector.wittMul_zero`, `C_neg`, `WittVector.polyOfInterest_vars_eq`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom`, `pderiv_inr_universalFactorizationMap_X`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul`, `WittVector.wittNeg_zero`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `MonomialOrder.sPolynomial_monomial_mul'`, `WeierstrassCurve.Jacobian.polynomialX_eq`, `transcendental_X`, `psum_eq_mul_esymm_sub_sum`, `Algebra.Generators.H1Cotangent.δ_eq_δAux`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `WittVector.bind₁_onePoly_wittPolynomial`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `support_sub`, `WittVector.wittOne_zero_eq_one`, `CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst`, `AlgebraicGeometry.AffineSpace.over_over`, `WittVector.bind₁_zero_wittPolynomial`, `IsTranscendenceBasis.mvPolynomial'`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp`, `StandardEtalePresentation.toPresentation_val`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `Polynomial.homogenize_sub`, `IsHomogeneous.eq_zero_of_forall_eval_eq_zero`, `Algebra.mvPolynomial`, `Algebra.SubmersivePresentation.ofSubsingleton_σ'`, `degreeOf_sub_lt`, `universalFactorizationMapPresentation_algebra_smul`, `LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis`, `totalDegree_sub_C_le`, `eval₂_C_mk_eq_zero`, `universalFactorizationMap_freeMonic`, `Algebra.Generators.Hom.toAlgHom_monomial`, `universalFactorizationMapPresentation_val`, `MonomialOrder.leadingCoeff_sub_of_lt`, `universalFactorizationMapPresentation_σ'`, `KaehlerDifferential.mvPolynomialBasis_repr_symm_single`, `AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `Algebra.Presentation.quotientEquiv_mk`, `MonomialOrder.div`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over`, `WittVector.mul_polyOfInterest_aux5`, `irreducible_sumSMulXSMulY`, `MonomialOrder.degree_X_add_C`, `isJacobsonRing_MvPolynomial_fin`, `MonomialOrder.degree_sub_leadingTerm_lt_degree`, `transcendental_supported_polynomial_aeval_X_iff`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over`, `StandardEtalePresentation.toPresentation_relation`, `Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_val`, `C_sub`, `quotientEquivQuotientMvPolynomial_rightInverse`, `WittVector.mul_polyOfInterest_aux3`, `WittVector.verschiebungPoly_zero`, `universalFactorizationMapPresentation_jacobiMatrix`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul`, `C_dvd_iff_zmod`, `MvRatFunc.rank_eq_max_lift`, `WittVector.wittOne_pos_eq_zero`, `IsHomogeneous.neg`, `algebraicIndependent_comp_subtype`, `rank_eq`, `RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`, `finrank_eq_one`, `trdeg_of_isDomain`, `transcendental_supported_X`, `degreeOf_neg`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `IsSymmetric.sub`, `Algebra.Generators.comp_σ`, `Algebra.Presentation.instFinitePresentationQuotientOfFinite`, `WittVector.wittSub_zero`, `WittVector.wittZero_eq_zero`, `exists_integral_inj_algHom_of_fg`, `Matrix.charpoly.univ_coeff_card`, `MonomialOrder.degree_sub_of_lt`, `Algebra.Generators.H1Cotangent.equiv_apply`, `wittPolynomial_eq_sum_C_mul_X_pow`, `instFreeMvPolynomialKaehlerDifferential`, `IsSymmetric.neg`, `rank_mvPolynomial_mvPolynomial`, `Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`, `MonomialOrder.degree_sub_leadingTerm_lt_iff`, `MonomialOrder.degree_sub_leadingTerm_le`, `rank_eq_lift`, `Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det`, `WittVector.wittAdd_zero`, `Polynomial.homogenize_neg`, `Algebra.Presentation.mem_ker_naive`, `instIsPushoutFractionRingMvPolynomial_1`, `MonomialOrder.sPolynomial_mul_monomial`, `Algebra.Generators.toExtension_commRing`, `Algebra.Generators.C_mul_X_sub_one_mem_ker`, `universalFactorizationMapPresentation_jacobian`, `MonomialOrder.sPolynomial_leadingTerm_mul`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap`, `Polynomial.coeff_freeMonic`, `MonomialOrder.degree_sPolynomial`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'`, `eq_zero_of_eval_zero_at_prod_finset`, `transcendental_supported_polynomial_aeval_X`, `instIsPushoutFractionRingMvPolynomial`, `pderiv_inl_universalFactorizationMap_X`, `Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_neg` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`C_sub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`coeff_neg` 📖	mathematical	—	`coeff` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`Finsupp.neg_apply`
`coeff_sub` 📖	mathematical	—	`coeff` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`Finsupp.sub_apply`
`degreeOf_neg` 📖	mathematical	—	`degreeOf` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`degreeOf.eq_1` `degrees_neg`
`degreeOf_sub_le` 📖	mathematical	—	`degreeOf` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`sub_eq_add_neg` `degreeOf_neg` `degreeOf_add_le`
`degreeOf_sub_lt` 📖	mathematical	`coeff` `CommRing.toCommSemiring`	`degreeOf` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`degreeOf_lt_iff`
`degrees_neg` 📖	mathematical	—	`degrees` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`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` `CommRing.toRing` `instCommRingMvPolynomial` `Multiset.instUnion`	—	`degrees_def` `coeff_sub` `AddMonoidAlgebra.supDegree_sub_le`
`eval_neg` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `eval` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`eval₂_neg`
`eval_sub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `eval` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`eval₂_sub`
`eval₂Hom_X` 📖	mathematical	—	`eval₂` `Int.instCommSemiring` `CommRing.toCommSemiring` `MvPolynomial` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `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` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`RingHom.map_neg`
`eval₂_sub` 📖	mathematical	—	`eval₂` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`RingHom.map_sub`
`hom_C` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `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` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`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` `CommRing.toRing` `instCommRingMvPolynomial` `Finset.instUnion` `Finsupp.instDecidableEq`	—	`Finsupp.support_sub`
`totalDegree_neg` 📖	mathematical	—	`totalDegree` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`support_neg`
`totalDegree_sub` 📖	mathematical	—	`totalDegree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial`	—	`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` `CommRing.toRing` `instCommRingMvPolynomial` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `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` `Ring.toAddCommGroup` `CommRing.toRing` `instCommRingMvPolynomial`	—	`degrees_neg`
`vars_sub_of_disjoint` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `vars` `CommRing.toCommSemiring`	`MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial` `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` `CommRing.toRing` `instCommRingMvPolynomial` `Finset.instUnion`	—	`sub_eq_add_neg` `vars_neg` `vars_add_subset`

(root)

Definitions

Name	Category	Theorems
`CommRing` 📖	CompData	3 math math: `CommRing.toRing_injective`, `nonempty_commRing_iff`, `nonempty_commRing`

---

← Back to Index