Theorem Ideal.primesOver_bot

Modification history

2026-01-13 19:40
Mathlib/RingTheory/Ideal/GoingUp.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified Ideal.primesOver_botView on Github →
2025-12-03 17:53
Mathlib/RingTheory/Ideal/GoingUp.lean
feat(CyclotomicField): splitting of the prime `p` in a cyclotomic field `ℚ(ζₙ)` (#32217) …
Modified Ideal.primesOver_botView on Github →
2025-02-07 16:33
Mathlib/RingTheory/Ideal/GoingUp.lean
chore(RingTheory/Ideal/Over): factor going-up results out (#21497) …
Added Ideal.primesOver_botView on Github →