mathlib

1700b3c6 - chore(ring_theory/fractional_ideal): make `coe : ideal → fractional_ideal` a `coe_t` (#8529)

chore(ring_theory/fractional_ideal): make `coe : ideal → fractional_ideal` a `coe_t` (#8529) This noticeably speeds up elaboration of `dedekind_domain.lean`, since it discourages the elaborator from going down a (nearly?)-looping path. See also this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Priority.20of.20.60coe_sort_trans.60