mathlib3

2f588be3 - refactor(ring_theory/fractional_ideal): refactor coe_to_fractional_ideal lemmas (#18055)

refactor(ring_theory/fractional_ideal): refactor coe_to_fractional_ideal lemmas (#18055) Rename `coe_to_fractional_ideal` lemmas to `coe_ideal'` lemmas and extract `coe_ideal_inj` as standalone `eq_iff` lemmas.