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	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring coeff IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow	—	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 📖	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.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	IsNilpotent Polynomial instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring 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.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow 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.toPow 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.toPow 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.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	IsNilpotent Polynomial instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instMul X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	commute_X_pow isNilpotent_C_mul_pow_X_of_isNilpotent
isNilpotent_reflect_iff 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	IsNilpotent Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring reflect	—	le_or_gt coeff_reflect revAt_le Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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.toPow 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.toPow	—	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 📖	mathematical	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.toPow SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	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.toPow divByMonic X	—	modByMonic_add_div 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.toPow	—	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.toPow	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 CommSemiring.toSemiring CommRing.toCommSemiring 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 CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	LT.lt.ne' Mathlib.Tactic.Contrapose.contrapose₃ instReflLe

---

← Back to Index