mathlib
18d031d1 - fix(ring_theory/dedekind_domain): Speed up ideal.unique_factorization_monoid (#9243)

Commit
4 years ago
fix(ring_theory/dedekind_domain): Speed up ideal.unique_factorization_monoid (#9243) The old proof was causing timeouts in CI. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Timeouts.20in.20ring_theory.2Fdedekind_domain.2Elean.3A664.3A9/near/253579691)
Author
Parents
Loading