Mathlib v3 is deprecated. Go to Mathlib v4

Theorem irreducible_pow_sup_of_ge

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_of_ge View on Github →