Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 14:30 0c6f0c2a

View on Github →

feat(ring_theory/dedekind_domain/ideal): add lemmas about sup of ideal with irreducible (#12859) These results were originally in #9345.

Estimated changes