nilpotency → normalizer_condition

Stream: maths

[Joachim Breitner]

Hallelujah, after about a week, I managed to prove the first implication in the list of equivalent conditions for nilpotency that Kevin suggested I work on, namely is_nilpotent G → normalizer_condition G.
But there is so much ugliness in my beginner proofs, of course, both in how I use lean and in how I use the math. I guess I should clean it up as far as I can, create a PR, and learn as the mathlib community will review my 330 lines to 30 :-)

[Joachim Breitner]

Is it preferred to submit helper lemmas, in particular those that would go into more basic lean files, one at a time?

[Alex J. Best]

One PR at a time might get a bit unwieldy, maybe groups of 5-10 would be a good number to review if you can find loose groups of somewhat related lemmas of that size

[Oliver Nash]

If there was a sensible lump of code that was, say, 50 lines then that might be a good initial PR for this work.

[Oliver Nash]

Also, congratulations and thanks. We need to fill all these gaps!