Commit 2021-09-10 16:18 d2afdc59

View on Github →

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)

Estimated changes

Modified src/algebra/associated.lean

added theorem multiset.prod_ne_zero_of_prime

Modified src/ring_theory/dedekind_domain.lean

added theorem count_le_of_ideal_ge

added theorem factors_prod_factors_eq_factors

added theorem prod_factors_eq_self

added theorem sup_eq_prod_inf_factors

Modified src/ring_theory/unique_factorization_domain.lean

added theorem unique_factorization_monoid.zero_not_mem_factors