mathlib3

a895300a - chore(ring_theory/fractional_ideal): prefer `(⊤ : ideal R)` over `1` (#8298)

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`.