Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 08:57 158263c1

View on Github →

feat(ring_theory): Nilradical and reduced ring (#10576)

Estimated changes

Modified src/ring_theory/nilpotent.lean

modified theorem is_nilpotent.eq_zero

modified theorem is_nilpotent_iff_eq_zero

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