Commit 2021-07-16 17:58 a895300a

chore(ring_theory/fractional_ideal): prefer (⊤ : ideal R) over 1 (#8298) fractional_ideal.lean sometimes used 1 to denote the ideal of R containing each element of R. This PR should replace all remaining usages with ⊤ : ideal R, following the convention in the rest of mathlib. Also a little simp lemma coe_ideal_top which was the motivation, since the proof should have been, and is now by refl.