Mathlib v3 is deprecated. Go to Mathlib v4

Theorem irreducible_pow_sup

Modification history

2022-03-28 14:30

src/ring_theory/dedekind_domain/ideal.lean

feat(ring_theory/dedekind_domain/ideal): add lemmas about sup of ideal with irreducible (#12859) …

Added irreducible_pow_sup View on Github →