Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-10 03:41 9fc0f227

View on Github →

feat(ring_theory/noetherian): The nilradical of a noetherian ring is nilpotent (#16881)

Estimated changes

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.sum_eq_sup

Modified src/ring_theory/noetherian.lean

added theorem ideal.exists_radical_pow_le_of_fg

added theorem is_noetherian_ring.is_nilpotent_nilradical