mathlib

6eb8d414 - chore(ring_theory/dedekind_domain): speed up `dedekind_domain.lean` (#9232)

chore(ring_theory/dedekind_domain): speed up `dedekind_domain.lean` (#9232) @eric-wieser [noticed that `dedekind_domain.lean`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Timeouts.20in.20ring_theory.2Fdedekind_domain.2Elean.3A664.3A9) was compiling slowly and on the verge of a timeout. @kbuzzard, @sgouezel and I reworked some definitions to make everything elaborate much faster: `is_dedekind_domain_inv_iff`, `mul_inv_cancel_of_le_one` and `ideal.unique_factorization_monoid` went from over 10 seconds on my machine to less than 3 seconds. No other declaration in that file now takes over 2 seconds on my machine. Apart from the three declarations getting new proofs, I also made the following changes: * The operations on `localization` (`has_add`, `has_mul`, `has_one`, `has_zero`, `has_neg`, `npow` and `localization.inv`) are now `@[irreducible]` * `fraction_ring.field` copies its field from `localization.comm_ring` for faster unification (less relevant after the previous change) * Added `fractional_ideal.map_mem_map` and `fractional_ideal.map_injective` to simplify the proof of `is_dedekind_domain_inv_iff`. * Split the proof of `matrix.exists_mul_vec_eq_zero_iff` into two parts to speed it up Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>