mathlib3

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

feat(ring_theory/artinian): is_nilpotent_jacobson (#9153) Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>