Commit 2024-10-07 17:59 5151ec1c

View on Github →

feat(RingTheory/Ideal/Operations): drop IsDedekindDomain assumptions of some lemmas and move them to Ideal/Operations.lean (#17460) Drop [IsDedekindDomain R] assumptions of some lemmas about ideal pow le a prime ideal and move them to RingTheory/Ideal/Operations.lean. Also add a lemma about product of elements in a prime ideal.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

deleted theorem Ideal.le_of_pow_le_prime

deleted theorem Ideal.pow_le_prime_iff

deleted theorem Ideal.prod_le_prime

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.IsPrime.le_of_pow_le

added theorem Ideal.IsPrime.pow_le_iff

added theorem Ideal.IsPrime.prod_mem_iff