Defs

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

Statistics

Metric	Count
Definitions IsRadical, nilpotencyClass	2
Theorems isNilpotent_mul_left, isNilpotent_mul_right, map, map_iff, isNilpotent_mul_unit_of_commute_iff, isNilpotent_unit_mul_of_commute_iff, eq_zero_of_nilpotencyClass_eq_one, instIsReducedForall, isNilpotent_of_pos_nilpotencyClass, isRadical_iff_pow_one_lt, isReduced_of_injective, nilpotencyClass_eq_one, nilpotencyClass_eq_succ_iff, nilpotencyClass_eq_zero_of_subsingleton, nilpotencyClass_zero, pos_nilpotencyClass_iff, pow_nilpotencyClass, pow_pred_nilpotencyClass	18
Total	20

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_mul_left 📖	—	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—	eq isNilpotent_mul_right symm
isNilpotent_mul_right 📖	—	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—	mul_pow MulZeroClass.zero_mul

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	IsNilpotent MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	DFunLike.coe	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass
map_iff 📖	mathematical	DFunLike.coe	IsNilpotent MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass map

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_mul_unit_of_commute_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	IsNilpotent MulZeroClass.toZero Monoid.toNatPow	—	Commute.mul_pow mul_left_eq_zero pow
isNilpotent_unit_mul_of_commute_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	IsNilpotent MulZeroClass.toZero Monoid.toNatPow	—	isNilpotent_mul_unit_of_commute_iff

(root)

Definitions

Name	Category	Theorems
IsRadical 📖	MathDef	9 math math: UniqueFactorizationMonoid.isRadical_radical, isRadical_iff_squarefree_or_zero, isRadical_iff_squarefree_of_ne_zero, zero_isRadical_iff, minpoly.isRadical, isRadical_iff_span_singleton, Squarefree.isRadical, Prime.isRadical, isRadical_iff_pow_one_lt
nilpotencyClass 📖	CompOp	6 math math: pos_nilpotencyClass_iff, nilpotencyClass_eq_one, pow_nilpotencyClass, nilpotencyClass_zero, nilpotencyClass_eq_zero_of_subsingleton, nilpotencyClass_eq_succ_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_nilpotencyClass_eq_one 📖	—	nilpotencyClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	—	isNilpotent_of_pos_nilpotencyClass pow_nilpotencyClass pow_one
instIsReducedForall 📖	mathematical	IsReduced	Pi.instZero Pi.instPow	—	IsReduced.eq_zero
isNilpotent_of_pos_nilpotencyClass 📖	mathematical	nilpotencyClass	IsNilpotent	—	Set.not_nonempty_iff_eq_empty Nat.sInf_empty
isRadical_iff_pow_one_lt 📖	mathematical	—	IsRadical semigroupDvd Monoid.toSemigroup Monoid.toNatPow	—	Nat.pow_imp_self_of_one_lt dvd_mul_of_dvd_left
isReduced_of_injective 📖	mathematical	DFunLike.coe	IsReduced MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	map_zero MonoidWithZeroHomClass.toZeroHomClass IsNilpotent.eq_zero IsNilpotent.map
nilpotencyClass_eq_one 📖	mathematical	—	nilpotencyClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	eq_zero_of_nilpotencyClass_eq_one nilpotencyClass_zero
nilpotencyClass_eq_succ_iff 📖	mathematical	—	nilpotencyClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	pow_eq_zero_of_le Nat.sInf_upward_closed_eq_succ_iff
nilpotencyClass_eq_zero_of_subsingleton 📖	mathematical	—	nilpotencyClass	—	Set.eq_univ_iff_forall csInf_univ
nilpotencyClass_zero 📖	mathematical	—	nilpotencyClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	nilpotencyClass_eq_succ_iff zero_add pow_one pow_zero NeZero.one
pos_nilpotencyClass_iff 📖	mathematical	—	nilpotencyClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid IsNilpotent	—	isNilpotent_of_pos_nilpotencyClass pow_nilpotencyClass one_ne_zero NeZero.one pow_zero
pow_nilpotencyClass 📖	mathematical	IsNilpotent	nilpotencyClass	—	Nat.sInf_mem
pow_pred_nilpotencyClass 📖	—	IsNilpotent MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	—	nilpotencyClass_eq_succ_iff pos_nilpotencyClass_iff

---

← Back to Index