Nilpotent

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

Statistics

Metric	Count
Definitions	0
Theorems instIsLocalHomRingHomAlgebraMap, instIsLocalHomRingHomC, instIsReduced, isNilpotent_iff, isUnit_iff, isUnit_iff_eq_C_of_isReduced, isUnit_iff_totalDegree_of_isReduced	7
Total	7

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalHomRingHomAlgebraMap 📖	mathematical	—	IsLocalHom MvPolynomial CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike algebraMap algebra Algebra.id	—	instIsLocalHomRingHomC
instIsLocalHomRingHomC 📖	mathematical	—	IsLocalHom MvPolynomial CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike C	—	coeff_C
instIsReduced 📖	mathematical	—	IsReduced MvPolynomial CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring	—	—
isNilpotent_iff 📖	mathematical	—	IsNilpotent MvPolynomial CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring coeff	—	exists_fin_rename IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass rename_injective Finite.of_fintype CanLift.prf Function.instCanLiftForallEmbeddingCoeInjective coeff_rename_embDomain coeff_rename_eq_zero Finsupp.embDomain_eq_mapDomain
isUnit_iff 📖	mathematical	—	IsUnit MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero IsNilpotent NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow	—	IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.coeff_isUnit_isNilpotent_of_isUnit AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass optionEquivLeft_coeff_some_coeff_none Finsupp.equivMapDomain_eq_mapDomain coeff_rename_mapDomain Equiv.injective coeff_sub coeff_C sub_self sub_zero sub_add_cancel IsNilpotent.isUnit_add_right_of_commute Commute.all
isUnit_iff_eq_C_of_isReduced 📖	mathematical	—	IsUnit MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	isUnit_iff_totalDegree_of_isReduced totalDegree_eq_zero_iff_eq_C coeff_zero_C
isUnit_iff_totalDegree_of_isReduced 📖	mathematical	—	IsUnit MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero totalDegree	—	totalDegree_eq_zero_iff not_imp_comm isUnit_iff

---

← Back to Index