Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-15 10:33 bb38ce96

View on Github →

feat(ring_theory/artinian): is_nilpotent_jacobson (#9153)

Estimated changes

Modified src/ring_theory/artinian.lean

added theorem is_artinian.monotone_stabilizes

added theorem is_artinian.set_has_minimal

added theorem is_artinian_ring.is_nilpotent_jacobson_bot