Theorem Ideal.add_pow_mem_of_pow_mem_of_le

Modification history

2024-04-01 16:53
Mathlib/RingTheory/Ideal/Basic.lean
feat(Mathlib/RingTheory/Ideal/Operations): simplify definition of radical (#11723) …
Added Ideal.add_pow_mem_of_pow_mem_of_leView on Github →