Commit 2025-06-06 16:43 48cebe31

View on Github →

feat(Ideal/Int): some results about ideals of or ideals of extensions of (#25528) Mainly we add the instance that Ideal.span {(p : ℤ)} is maximal is p is a prime and prove some results about the smallest positive integer contained in an ideal.

Estimated changes