chore(ring_theory/fractional_ideal): remove instance name (#18305)

leanprover-community · Jan 30, 2023 · 48cb182 · 48cb182
1 parent fac3690
commit 48cb182
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean
@@ -912,8 +912,7 @@ lemma fractional_div_of_nonzero {I J : fractional_ideal R₁⁰ K} (h : J ≠ 0)
 I.is_fractional.div_of_nonzero J.is_fractional $ λ H, h $
   coe_to_submodule_injective $ H.trans coe_zero.symm
 
-noncomputable instance fractional_ideal_has_div :
-  has_div (fractional_ideal R₁⁰ K) :=
+noncomputable instance : has_div (fractional_ideal R₁⁰ K) :=
 ⟨ λ I J, if h : J = 0 then 0 else ⟨I / J, fractional_div_of_nonzero h⟩ ⟩
 
 variables {I J : fractional_ideal R₁⁰ K} [ J ≠ 0 ]