Commit 2021-09-22 16:35 6eb8d414

chore(ring_theory/dedekind_domain): speed up dedekind_domain.lean (#9232) @eric-wieser noticed that dedekind_domain.lean 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