Theorem Ideal.isMaximal_of_mem_primesOver

Modification history

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