Theorem Ideal.pow_mem_of_pow_mem

Modification history

2024-10-29 15:17

Mathlib/RingTheory/Ideal/Basic.lean

chore(RingTheory/Ideal): split up `Ideal/Basic.lean` (#18383) …

Modified Ideal.pow_mem_of_pow_mem View on Github →

2024-04-01 16:53

Mathlib/RingTheory/Ideal/Basic.lean

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

Added Ideal.pow_mem_of_pow_mem View on Github →