Commit 2023-03-12 19:12 e5b2bcd6

View on Github →

feat: port RingTheory.Nilpotent (#2829)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Nilpotent.lean

added theorem Commute.isNilpotent_add

added theorem Commute.isNilpotent_mul_left

added theorem Commute.isNilpotent_mul_right

added theorem Commute.isNilpotent_sub

added theorem IsNilpotent.eq_zero

added theorem IsNilpotent.map

added theorem IsNilpotent.mk

added theorem IsNilpotent.neg

added theorem IsNilpotent.zero

added def IsNilpotent

added def IsRadical

added theorem LinearMap.isNilpotent_mulLeft_iff

added theorem LinearMap.isNilpotent_mulRight_iff

added theorem Module.End.IsNilpotent.mapQ

added theorem RingHom.ker_isRadical_iff_reduced_of_surjective

added theorem isNilpotent_iff_eq_zero

added theorem isNilpotent_neg_iff

added theorem isRadical_iff_pow_one_lt

added theorem isRadical_iff_span_singleton

added theorem isReduced_iff_pow_one_lt

added theorem isReduced_of_injective

added theorem mem_nilradical

added theorem nilpotent_iff_mem_prime

added def nilradical

added theorem nilradical_eq_infₛ

added theorem nilradical_eq_zero

added theorem nilradical_le_prime

added theorem zero_isRadical_iff