Theorem Ideal.pow_le_prime_iff

Modification history

2024-10-07 17:59

Mathlib/RingTheory/DedekindDomain/Ideal.lean

feat(RingTheory/Ideal/Operations): drop `IsDedekindDomain` assumptions of some lemmas and move them to `Ideal/Operations.lean` (#17460) …

Deleted Ideal.pow_le_prime_iff View on Github →

2023-06-05 16:53

Mathlib/RingTheory/DedekindDomain/Ideal.lean

feat: port RingTheory.DedekindDomain.Ideal (#4630) …

Added Ideal.pow_le_prime_iff View on Github →