Commit 2024-04-01 16:53 ab5ca959

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

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