Theorem Ideal.ne_bot_of_mem_primesOver

Modification history

2025-09-22 16:24
Mathlib/RingTheory/Ideal/Over.lean
feat(Ring/DedekindDomain): formula for the splitting of prime ideals in an extension (#27105) …
Added Ideal.ne_bot_of_mem_primesOverView on Github →