Theorem Ideal.prime_of_mem_primesOver

Modification history

2025-12-03 17:53
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(CyclotomicField): splitting of the prime `p` in a cyclotomic field `ℚ(ζₙ)` (#32217) …
Added Ideal.prime_of_mem_primesOverView on Github →