Nilpotent

📁 Source: Mathlib/RingTheory/Polynomial/Nilpotent.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_isUnit_isNilpotent_of_isUnit, instIsLocalHomRingHomAlgebraMap, instIsLocalHomRingHomC, isNilpotent_C_iff, isNilpotent_C_mul_pow_X_of_isNilpotent, isNilpotent_X_mul_iff, isNilpotent_aeval_sub_of_isNilpotent_sub, isNilpotent_iff, isNilpotent_monomial_iff, isNilpotent_mul_X_iff, isNilpotent_pow_X_mul_C_of_isNilpotent, isNilpotent_reflect_iff, isNilpotent_reverse_iff, isUnit_C_add_X_mul_iff, isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub, isUnit_iff', isUnit_iff_coeff_isUnit_isNilpotent, isUnit_of_coeff_isUnit_isNilpotent, not_isUnit_of_degree_pos_of_isReduced, not_isUnit_of_natDegree_pos_of_isReduced	20
Total	20

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_isUnit_isNilpotent_of_isUnit 📖	mathematical	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	coeff IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow	—	IsUnit.exists_right_inv IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid mul_coeff_zero coeff_one_zero nilpotent_iff_mem_prime Ideal.instIsTwoSided_1 Nat.WithBot.add_eq_zero_iff degree_mul Ideal.Quotient.noZeroDivisors map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass degree_one IsDomain.toNontrivial Ideal.Quotient.isDomain coeff_eq_zero_of_degree_lt WithBot.coe_pos Ne.bot_lt Ideal.mk_ker RingHom.mem_ker coeff_map coe_mapRingHom
instIsLocalHomRingHomAlgebraMap 📖	mathematical	—	IsLocalHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike algebraMap algebraOfAlgebra Algebra.id	—	instIsLocalHomRingHomC
instIsLocalHomRingHomC 📖	mathematical	—	IsLocalHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike C	—	coeff_C
isNilpotent_C_iff 📖	mathematical	—	IsNilpotent Polynomial instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	C_eq_zero
isNilpotent_C_mul_pow_X_of_isNilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Polynomial instZero semiring instMul DFunLike.coe RingHom RingHom.instFunLike C X	—	Commute.isNilpotent_mul_right Commute.symm commute_X_pow C_pow C_0
isNilpotent_X_mul_iff 📖	mathematical	—	IsNilpotent Polynomial instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instMul X	—	Commute.isNilpotent_mul_left_iff commute_X Commute.mul_pow MulZeroClass.mul_zero
isNilpotent_aeval_sub_of_isNilpotent_sub 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	Commute.isNilpotent_mul_left Commute.all
isNilpotent_iff 📖	mathematical	—	IsNilpotent Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing coeff	—	coeff_zero_eq_aeval_zero isNilpotent_C_iff eval_pow eval_add eval_C zero_add eval_zero coeff_add coeff_C_zero coeff_C_succ add_zero add_sub_cancel_right Commute.isNilpotent_sub Commute.all mul_coeff_zero coeff_X_zero MulZeroClass.mul_zero coeff_mul_X isNilpotent_mul_X_iff sum_monomial_eq isNilpotent_sum
isNilpotent_monomial_iff 📖	mathematical	—	IsNilpotent Polynomial instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	monomial_pow
isNilpotent_mul_X_iff 📖	mathematical	—	IsNilpotent Polynomial instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instMul X	—	commute_X isNilpotent_X_mul_iff
isNilpotent_pow_X_mul_C_of_isNilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Polynomial instZero semiring instMul X DFunLike.coe RingHom RingHom.instFunLike C	—	commute_X_pow isNilpotent_C_mul_pow_X_of_isNilpotent
isNilpotent_reflect_iff 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	IsNilpotent Polynomial instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring reflect	—	le_or_gt coeff_reflect revAt_le Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd tsub_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE coeff_eq_zero_of_natDegree_lt lt_of_le_of_lt revAt_eq_self_of_lt
isNilpotent_reverse_iff 📖	mathematical	—	IsNilpotent Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring reverse	—	isNilpotent_reflect_iff le_refl
isUnit_C_add_X_mul_iff 📖	mathematical	—	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instAdd DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C instMul X IsNilpotent instZero Monoid.toNatPow	—	coeff_add coeff_C_succ coeff_X_mul zero_add coeff_C_zero mul_coeff_zero coeff_X_zero MulZeroClass.zero_mul add_zero
isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	—	add_sub_cancel IsNilpotent.isUnit_add_left_of_commute isNilpotent_aeval_sub_of_isNilpotent_sub Commute.all
isUnit_iff' 📖	mathematical	—	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsNilpotent Ring.toSemiring CommRing.toRing instZero Monoid.toNatPow divByMonic X	—	modByMonic_add_div monic_X modByMonic_X
isUnit_iff_coeff_isUnit_isNilpotent 📖	mathematical	—	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring coeff IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow	—	coeff_isUnit_isNilpotent_of_isUnit isUnit_of_coeff_isUnit_isNilpotent
isUnit_of_coeff_isUnit_isNilpotent 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring coeff IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow	Polynomial semiring	—	Nat.strong_induction_on eq_C_of_natDegree_eq_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass lt_of_le_of_lt eraseLead_natDegree_le zero_lt_one Nat.instZeroLEOneClass eraseLead_coeff_of_ne ne_of_lt coeff_eq_zero_of_natDegree_lt eraseLead_add_monomial_natDegree_leadingCoeff C_mul_X_pow_eq_monomial IsNilpotent.isUnit_add_left_of_commute isNilpotent_C_mul_pow_X_of_isNilpotent Commute.all
not_isUnit_of_degree_pos_of_isReduced 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree CommSemiring.toSemiring CommRing.toCommSemiring	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	not_isUnit_of_natDegree_pos_of_isReduced natDegree_pos_iff_degree_pos
not_isUnit_of_natDegree_pos_of_isReduced 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	LT.lt.ne' Mathlib.Tactic.Contrapose.contrapose₃

---

← Back to Index