Theorem Ideal.exists_pow_le_of_le_radical_of_fg_radical

Modification history

2024-10-26 13:22

Mathlib/RingTheory/Finiteness.lean

chore(RingTheory): move `Ideal.exists_pow_le_of_le_radical_of_fG` (#18189) …

Added Ideal.exists_pow_le_of_le_radical_of_fg_radical View on Github →