Theorem Ideal.mem_primesOver_iff_mem_normalizedFactors

Modification history

2025-09-16 15:34
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (#26101) …
Added Ideal.mem_primesOver_iff_mem_normalizedFactorsView on Github →