Commit 2026-06-22 14:05 9f59f3b8
View on Github →feat(RingTheory/Ideal/Operations): pow_eq_bot (#40836)
We add
theorem Ideal.pow_eq_bot.{u} {R : Type u} [Semiring R] {I : Ideal R} [isReduced R] {n : ℕ} (hn : n ≠ 0) :
I ^ n = ⊥ ↔ I = ⊥
feat(RingTheory/Ideal/Operations): pow_eq_bot (#40836)
We add
theorem Ideal.pow_eq_bot.{u} {R : Type u} [Semiring R] {I : Ideal R} [isReduced R] {n : ℕ} (hn : n ≠ 0) :
I ^ n = ⊥ ↔ I = ⊥