Mathlib v3 is deprecated. Go to Mathlib v4

Theorem count_le_of_ideal_ge

Modification history

2021-09-10 16:18

src/ring_theory/dedekind_domain.lean

feat(ring_theory/dedekind_domain): add proof that `I \sup J` is the product of `factors I \inf factors J` for `I, J` ideals in a Dedekind Domain (#9055)

Added count_le_of_ideal_ge View on Github →