feat(Mathlib/RingTheory/Ideal/Operations): simplify definition of radical

[AntoineChambert-Loir]

• add_pow_add_pred_mem_of_pow_mem says that (a + b) ^ (m + n - 1) belongs to an ideal I if a ^ m and b ^ n belong to that ideal
• Commute.add_pow_add_pred_eq_zero_of_pow_eq_zero says that (a + b) ^ (m + n - 1) = 0 if a ^ m = 0 and b^ n = 0
• this is used to simplify the definition of docs#Ideal.radical and the definition of docs#Commute.isNilpotent_add

---

[mathlib-bors[bot]]

:v: AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[AntoineChambert-Loir]

Actually, I just realized (ON made me…) that docs#Commute.isNilpotent_add merits being adjusted as well. I need a few hours…

[mathlib-bors[bot]]

:v: AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[AntoineChambert-Loir]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style