mathlib

9cc44ba2 - feat(ring_theory/nilpotent): basic results about nilpotency in associative rings (#8055)