refactor(ring_theory/fractional_ideal): refactor coe_to_fractional_id…

…eal lemmas (#18055)

Rename `coe_to_fractional_ideal` lemmas to `coe_ideal'` lemmas and extract `coe_ideal_inj` as standalone `eq_iff` lemmas.

src/ring_theory/class_group.lean

@@ -159,8 +159,7 @@ by rw [class_group.mk, monoid_hom.comp_apply, ← monoid_hom.comp_apply (units.m
 /-- Send a nonzero integral ideal to an invertible fractional ideal. -/
 noncomputable def fractional_ideal.mk0 [is_dedekind_domain R] :
   (ideal R)⁰ →* (fractional_ideal R⁰ K)ˣ :=
-{ to_fun := λ I, units.mk0 I ((fractional_ideal.coe_to_fractional_ideal_ne_zero (le_refl R⁰)).mpr
-    (mem_non_zero_divisors_iff_ne_zero.mp I.2)),
+{ to_fun   := λ I, units.mk0 I (coe_ideal_ne_zero.mpr $ mem_non_zero_divisors_iff_ne_zero.mp I.2),
   map_one' := by simp,
   map_mul' := λ x y, by simp }
 
@@ -170,8 +169,7 @@ rfl
 
 lemma fractional_ideal.canonical_equiv_mk0 [is_dedekind_domain R]
   (K' : Type*) [field K'] [algebra R K'] [is_fraction_ring R K'] (I : (ideal R)⁰) :
-  fractional_ideal.canonical_equiv R⁰ K K' (fractional_ideal.mk0 K I) =
-    fractional_ideal.mk0 K' I :=
+  fractional_ideal.canonical_equiv R⁰ K K' (fractional_ideal.mk0 K I) = fractional_ideal.mk0 K' I :=
 by simp only [fractional_ideal.coe_mk0, coe_coe, fractional_ideal.canonical_equiv_coe_ideal]
 
 @[simp] lemma fractional_ideal.map_canonical_equiv_mk0 [is_dedekind_domain R]
@@ -181,8 +179,7 @@ by simp only [fractional_ideal.coe_mk0, coe_coe, fractional_ideal.canonical_equi
 units.ext (fractional_ideal.canonical_equiv_mk0 K K' I)
 
 /-- Send a nonzero ideal to the corresponding class in the class group. -/
-noncomputable def class_group.mk0 [is_dedekind_domain R] :
-  (ideal R)⁰ →* class_group R :=
+noncomputable def class_group.mk0 [is_dedekind_domain R] : (ideal R)⁰ →* class_group R :=
 class_group.mk.comp (fractional_ideal.mk0 (fraction_ring R))
 
 @[simp] lemma class_group.mk_mk0 [is_dedekind_domain R] (I : (ideal R)⁰):
@@ -202,8 +199,7 @@ begin
 end
 
 lemma class_group.mk0_eq_mk0_iff_exists_fraction_ring [is_dedekind_domain R] {I J : (ideal R)⁰} :
-  class_group.mk0 I = class_group.mk0 J ↔
-    ∃ (x ≠ (0 : K)), span_singleton R⁰ x * I = J :=
+  class_group.mk0 I = class_group.mk0 J ↔ ∃ (x ≠ (0 : K)), span_singleton R⁰ x * I = J :=
 begin
   refine (class_group.equiv K).injective.eq_iff.symm.trans _,
   simp only [class_group.equiv_mk0, quotient_group.mk'_eq_mk', mem_principal_ideals_iff,
@@ -305,8 +301,7 @@ begin
   simp [hx']
 end
 
-lemma class_group.mk0_eq_one_iff [is_dedekind_domain R]
-  {I : ideal R} (hI : I ∈ (ideal R)⁰) :
+lemma class_group.mk0_eq_one_iff [is_dedekind_domain R] {I : ideal R} (hI : I ∈ (ideal R)⁰) :
   class_group.mk0 ⟨I, hI⟩ = 1 ↔ I.is_principal :=
 class_group.mk_eq_one_iff.trans (coe_submodule_is_principal R _)
 
@@ -315,8 +310,7 @@ class_group.mk_eq_one_iff.trans (coe_submodule_is_principal R _)
 See `class_group.fintype_of_admissible` for a finiteness proof that works for rings of integers
 of global fields.
 -/
-noncomputable instance [is_principal_ideal_ring R] :
-  fintype (class_group R) :=
+noncomputable instance [is_principal_ideal_ring R] : fintype (class_group R) :=
 { elems := {1},
   complete :=
   begin
@@ -326,8 +320,7 @@ noncomputable instance [is_principal_ideal_ring R] :
   end }
 
 /-- The class number of a principal ideal domain is `1`. -/
-lemma card_class_group_eq_one [is_principal_ideal_ring R] :
-  fintype.card (class_group R) = 1 :=
+lemma card_class_group_eq_one [is_principal_ideal_ring R] : fintype.card (class_group R) = 1 :=
 begin
   rw fintype.card_eq_one_iff,
   use 1,

src/ring_theory/dedekind_domain/factorization.lean

@@ -89,7 +89,7 @@ lemma finite_mul_support_coe {I : ideal R} (hI : I ≠ 0) :
 begin
   rw mul_support,
   simp_rw [ne.def, zpow_coe_nat, ← fractional_ideal.coe_ideal_pow,
-    fractional_ideal.coe_ideal_eq_one_iff],
+    fractional_ideal.coe_ideal_eq_one],
   exact finite_mul_support hI,
 end
 

src/ring_theory/dedekind_domain/ideal.lean

@@ -266,8 +266,7 @@ begin
   refine is_noetherian_ring_iff.mpr ⟨λ (I : ideal A), _⟩,
   by_cases hI : I = ⊥,
   { rw hI, apply submodule.fg_bot },
-  have hI : (I : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 :=
-    (coe_to_fractional_ideal_ne_zero (le_refl (non_zero_divisors A))).mpr hI,
+  have hI : (I : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 := coe_ideal_ne_zero.mpr hI,
   exact I.fg_of_is_unit (is_fraction_ring.injective A (fraction_ring A)) (h.is_unit hI)
 end
 
@@ -292,11 +291,9 @@ begin
   rintros P P_ne hP,
   refine ideal.is_maximal_def.mpr ⟨hP.ne_top, λ M hM, _⟩,
   -- We may assume `P` and `M` (as fractional ideals) are nonzero.
-  have P'_ne : (P : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 :=
-    (coe_to_fractional_ideal_ne_zero (le_refl (non_zero_divisors A))).mpr P_ne,
+  have P'_ne : (P : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 := coe_ideal_ne_zero.mpr P_ne,
   have M'_ne : (M : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 :=
-    (coe_to_fractional_ideal_ne_zero (le_refl (non_zero_divisors A))).mpr
-      (lt_of_le_of_lt bot_le hM).ne',
+    coe_ideal_ne_zero.mpr (lt_of_le_of_lt bot_le hM).ne',
 
   -- In particular, we'll show `M⁻¹ * P ≤ P`
   suffices : (M⁻¹ * P : fractional_ideal A⁰ (fraction_ring A)) ≤ P,
@@ -390,7 +387,7 @@ begin
     have hM0 := (M.bot_lt_of_maximal hNF).ne',
     obtain ⟨x, hxM, hx1⟩ := this hM,
     refine ⟨x, inv_anti_mono _ _ ((coe_ideal_le_coe_ideal _).mpr hIM) hxM, hx1⟩;
-      apply coe_ideal_ne_zero; assumption },
+      rw coe_ideal_ne_zero; assumption },
 
   -- Let `a` be a nonzero element of `M` and `J` the ideal generated by `a`.
   intros M hM,
@@ -414,7 +411,7 @@ begin
       (λ h, hbJ $ h.symm ▸ J.zero_mem),
   -- Then `b a⁻¹ : K` is in `M⁻¹` but not in `1`.
   refine ⟨algebra_map A K b * (algebra_map A K a)⁻¹, (mem_inv_iff _).mpr _, _⟩,
-  { exact (coe_to_fractional_ideal_ne_zero le_rfl).mpr hM0.ne' },
+  { exact coe_ideal_ne_zero.mpr hM0.ne' },
   { rintro y₀ hy₀,
     obtain ⟨y, h_Iy, rfl⟩ := (mem_coe_ideal _).mp hy₀,
     rw [mul_comm, ← mul_assoc, ← ring_hom.map_mul],
@@ -436,7 +433,7 @@ end
 lemma one_mem_inv_coe_ideal {I : ideal A} (hI : I ≠ ⊥) :
   (1 : K) ∈ (I : fractional_ideal A⁰ K)⁻¹ :=
 begin
-  rw mem_inv_iff (coe_ideal_ne_zero hI),
+  rw mem_inv_iff (coe_ideal_ne_zero.mpr hI),
   intros y hy,
   rw one_mul,
   exact coe_ideal_le_one hy,
@@ -496,7 +493,7 @@ begin
   have x_mul_mem : ∀ b ∈ (I⁻¹ : fractional_ideal A⁰ K), x * b ∈ (I⁻¹ : fractional_ideal A⁰ K),
   { intros b hb,
     rw mem_inv_iff at ⊢ hx,
-    swap, { exact coe_ideal_ne_zero hI0 },
+    swap, { exact coe_ideal_ne_zero.mpr hI0 },
     swap, { exact hJ0 },
     simp only [mul_assoc, mul_comm b] at ⊢ hx,
     intros y hy,
@@ -534,7 +531,7 @@ begin
       span_singleton_mul_span_singleton, inv_mul_cancel, span_singleton_one],
   { exact mt ((injective_iff_map_eq_zero (algebra_map A K)).mp
       (is_fraction_ring.injective A K) _) ha },
-  { exact coe_ideal_ne_zero_iff.mp (right_ne_zero_of_mul hne) }
+  { exact coe_ideal_ne_zero.mp (right_ne_zero_of_mul hne) }
 end
 
 lemma mul_right_le_iff [is_dedekind_domain A] {J : fractional_ideal A⁰ K}
@@ -601,7 +598,7 @@ noncomputable instance fractional_ideal.semifield :
   div := (/),
   div_eq_mul_inv := fractional_ideal.div_eq_mul_inv,
   mul_inv_cancel := λ I, fractional_ideal.mul_inv_cancel,
-  .. fractional_ideal.comm_semiring, ..(coe_to_fractional_ideal_injective le_rfl).nontrivial }
+  .. fractional_ideal.comm_semiring, .. coe_ideal_injective.nontrivial }
 
 /-- Fractional ideals have cancellative multiplication in a Dedekind domain.
 
@@ -632,15 +629,14 @@ lemma ideal.dvd_iff_le {I J : ideal A} : (I ∣ J) ↔ J ≤ I :=
     by_cases hI : I = ⊥,
     { have hJ : J = ⊥, { rwa [hI, ← eq_bot_iff] at h },
       rw [hI, hJ] },
-    have hI' : (I : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 :=
-      (coe_to_fractional_ideal_ne_zero (le_refl (non_zero_divisors A))).mpr hI,
+    have hI' : (I : fractional_ideal A⁰ (fraction_ring A)) ≠ 0 := coe_ideal_ne_zero.mpr hI,
     have : (I : fractional_ideal A⁰ (fraction_ring A))⁻¹ * J ≤ 1 := le_trans
       (mul_left_mono (↑I)⁻¹ ((coe_ideal_le_coe_ideal _).mpr h))
       (le_of_eq (inv_mul_cancel hI')),
     obtain ⟨H, hH⟩ := le_one_iff_exists_coe_ideal.mp this,
     use H,
-    refine coe_to_fractional_ideal_injective (le_refl (non_zero_divisors A))
-      (show (J : fractional_ideal A⁰ (fraction_ring A)) = _, from _),
+    refine coe_ideal_injective
+      (show (J : fractional_ideal A⁰ (fraction_ring A)) = ↑(I * H), from _),
     rw [coe_ideal_mul, hH, ← mul_assoc, mul_inv_cancel hI', one_mul]
 end⟩
 

src/ring_theory/fractional_ideal.lean

@@ -108,8 +108,7 @@ variables [algebra R P] [loc : is_localization S P]
 This coercion is typically called `coe_to_submodule` in lemma names
 (or `coe` when the coercion is clear from the context),
 not to be confused with `is_localization.coe_submodule : ideal R → submodule R P`
-(which we use to define `coe : ideal R → fractional_ideal S P`,
-referred to as `coe_ideal` in theorem names).
+(which we use to define `coe : ideal R → fractional_ideal S P`).
 -/
 instance : has_coe (fractional_ideal S P) (submodule R P) := ⟨λ I, I.val⟩
 
@@ -156,8 +155,10 @@ lemma coe_to_submodule_injective :
   function.injective (coe : fractional_ideal S P → submodule R P) :=
 subtype.coe_injective
 
-lemma is_fractional_of_le_one (I : submodule R P) (h : I ≤ 1) :
-  is_fractional S I :=
+lemma coe_to_submodule_inj {I J : fractional_ideal S P} : (I : submodule R P) = J ↔ I = J :=
+coe_to_submodule_injective.eq_iff
+
+lemma is_fractional_of_le_one (I : submodule R P) (h : I ≤ 1) : is_fractional S I :=
 begin
   use [1, S.one_mem],
   intros b hb,
@@ -166,8 +167,8 @@ begin
   exact set.mem_range_self b',
 end
 
-lemma is_fractional_of_le {I : submodule R P} {J : fractional_ideal S P}
-  (hIJ : I ≤ J) : is_fractional S I :=
+lemma is_fractional_of_le {I : submodule R P} {J : fractional_ideal S P} (hIJ : I ≤ J) :
+  is_fractional S I :=
 begin
   obtain ⟨a, a_mem, ha⟩ := J.is_fractional,
   use [a, a_mem],
@@ -184,9 +185,9 @@ also called `coe_to_submodule` in theorem names.
 This map is available as a ring hom, called `fractional_ideal.coe_ideal_hom`.
 -/
 -- Is a `coe_t` rather than `coe` to speed up failing inference, see library note [use has_coe_t]
-instance coe_to_fractional_ideal : has_coe_t (ideal R) (fractional_ideal S P) :=
-⟨λ I, ⟨coe_submodule P I, is_fractional_of_le_one _
-  (by simpa using coe_submodule_mono P (le_top : I ≤ ⊤))⟩⟩
+instance : has_coe_t (ideal R) (fractional_ideal S P) :=
+⟨λ I, ⟨coe_submodule P I,
+  is_fractional_of_le_one _ $ by simpa using coe_submodule_mono P (le_top : I ≤ ⊤)⟩⟩
 
 @[simp, norm_cast] lemma coe_coe_ideal (I : ideal R) :
   ((I : fractional_ideal S P) : submodule R P) = coe_submodule P I := rfl
@@ -222,8 +223,7 @@ variables {S}
 @[simp, norm_cast] lemma coe_zero : ↑(0 : fractional_ideal S P) = (⊥ : submodule R P) :=
 submodule.ext $ λ _, mem_zero_iff S
 
-@[simp, norm_cast] lemma coe_to_fractional_ideal_bot : ((⊥ : ideal R) : fractional_ideal S P) = 0 :=
-rfl
+@[simp, norm_cast] lemma coe_ideal_bot : ((⊥ : ideal R) : fractional_ideal S P) = 0 := rfl
 
 variables (P)
 
@@ -235,22 +235,21 @@ include loc
 
 variables {P}
 
-lemma coe_to_fractional_ideal_injective (h : S ≤ non_zero_divisors R) :
+lemma coe_ideal_injective' (h : S ≤ non_zero_divisors R) :
   function.injective (coe : ideal R → fractional_ideal S P) :=
-λ I J heq, have
-  ∀ (x : R), algebra_map R P x ∈ (I : fractional_ideal S P) ↔
-             algebra_map R P x ∈ (J : fractional_ideal S P) :=
-λ x, heq ▸ iff.rfl,
-ideal.ext (by simpa only [mem_coe_ideal, exists_prop, exists_mem_to_map_eq P h] using this)
+λ _ _ h', ((coe_ideal_le_coe_ideal' S h).mp h'.le).antisymm ((coe_ideal_le_coe_ideal' S h).mp h'.ge)
 
-lemma coe_to_fractional_ideal_eq_zero {I : ideal R} (hS : S ≤ non_zero_divisors R) :
+lemma coe_ideal_inj' (h : S ≤ non_zero_divisors R) {I J : ideal R} :
+  (I : fractional_ideal S P) = J ↔ I = J :=
+(coe_ideal_injective' h).eq_iff
+
+@[simp] lemma coe_ideal_eq_zero' {I : ideal R} (h : S ≤ non_zero_divisors R) :
   (I : fractional_ideal S P) = 0 ↔ I = (⊥ : ideal R) :=
-⟨λ h, coe_to_fractional_ideal_injective hS h,
- λ h, by rw [h, coe_to_fractional_ideal_bot]⟩
+coe_ideal_inj' h
 
-lemma coe_to_fractional_ideal_ne_zero {I : ideal R} (hS : S ≤ non_zero_divisors R) :
+lemma coe_ideal_ne_zero' {I : ideal R} (h : S ≤ non_zero_divisors R) :
   (I : fractional_ideal S P) ≠ 0 ↔ I ≠ (⊥ : ideal R) :=
-not_iff_not.mpr (coe_to_fractional_ideal_eq_zero hS)
+not_iff_not.mpr $ coe_ideal_eq_zero' h
 
 omit loc
 
@@ -270,8 +269,7 @@ instance : has_one (fractional_ideal S P) :=
 
 variables (S)
 
-@[simp, norm_cast] lemma coe_ideal_top : ((⊤ : ideal R) : fractional_ideal S P) = 1 :=
-rfl
+@[simp, norm_cast] lemma coe_ideal_top : ((⊤ : ideal R) : fractional_ideal S P) = 1 := rfl
 
 lemma mem_one_iff {x : P} : x ∈ (1 : fractional_ideal S P) ↔ ∃ x' : R, algebra_map R P x' = x :=
 iff.intro (λ ⟨x', _, h⟩, ⟨x', h⟩) (λ ⟨x', h⟩, ⟨x', ⟨⟩, h⟩)
@@ -538,7 +536,7 @@ def coe_ideal_hom : ideal R →+* fractional_ideal S P :=
   map_add' := coe_ideal_sup,
   map_mul' := coe_ideal_mul,
   map_one' := by rw [ideal.one_eq_top, coe_ideal_top],
-  map_zero' := coe_to_fractional_ideal_bot }
+  map_zero' := coe_ideal_bot }
 
 lemma coe_ideal_pow (I : ideal R) (n : ℕ) : (↑(I^n) : fractional_ideal S P) = I^n :=
 (coe_ideal_hom S P).map_pow _ n
@@ -547,8 +545,7 @@ open_locale big_operators
 lemma coe_ideal_finprod [is_localization S P] {α : Sort*} {f : α → ideal R}
   (hS : S ≤ non_zero_divisors R) :
   ((∏ᶠ a : α, f a : ideal R) : fractional_ideal S P) = ∏ᶠ a : α, (f a : fractional_ideal S P) :=
-monoid_hom.map_finprod_of_injective (coe_ideal_hom S P).to_monoid_hom
-  (coe_to_fractional_ideal_injective hS) f
+monoid_hom.map_finprod_of_injective (coe_ideal_hom S P).to_monoid_hom (coe_ideal_injective' hS) f
 
 end order
 
@@ -815,19 +812,23 @@ end
 ⟨imp_of_not_imp_not _ _ (map_ne_zero _), λ hI, hI.symm ▸ map_zero h⟩
 
 lemma coe_ideal_injective : function.injective (coe : ideal R → fractional_ideal R⁰ K) :=
-injective_of_le_imp_le _ (λ _ _, (coe_ideal_le_coe_ideal _).mp)
+coe_ideal_injective' le_rfl
+
+lemma coe_ideal_inj {I J : ideal R} :
+  (I : fractional_ideal R⁰ K) = (J : fractional_ideal R⁰ K) ↔ I = J :=
+coe_ideal_inj' le_rfl
 
-@[simp] lemma coe_ideal_eq_zero_iff {I : ideal R} : (I : fractional_ideal R⁰ K) = 0 ↔ I = ⊥ :=
-coe_ideal_injective.eq_iff
+@[simp] lemma coe_ideal_eq_zero {I : ideal R} : (I : fractional_ideal R⁰ K) = 0 ↔ I = ⊥ :=
+coe_ideal_eq_zero' le_rfl
 
-lemma coe_ideal_ne_zero_iff {I : ideal R} : (I : fractional_ideal R⁰ K) ≠ 0 ↔ I ≠ ⊥ :=
-not_iff_not.mpr coe_ideal_eq_zero_iff
+lemma coe_ideal_ne_zero {I : ideal R} : (I : fractional_ideal R⁰ K) ≠ 0 ↔ I ≠ ⊥ :=
+coe_ideal_ne_zero' le_rfl
 
-lemma coe_ideal_ne_zero {I : ideal R} (hI : I ≠ ⊥) : (I : fractional_ideal R⁰ K) ≠ 0 :=
-coe_ideal_ne_zero_iff.mpr hI
+@[simp] lemma coe_ideal_eq_one {I : ideal R} : (I : fractional_ideal R⁰ K) = 1 ↔ I = 1 :=
+by simpa only [ideal.one_eq_top] using coe_ideal_inj
 
-@[simp] lemma coe_ideal_eq_one_iff {I : ideal R} : (I : fractional_ideal R⁰ K) = 1 ↔ I = 1 :=
-by simpa only [ideal.one_eq_top] using coe_ideal_injective.eq_iff
+lemma coe_ideal_ne_one {I : ideal R} : (I : fractional_ideal R⁰ K) ≠ 1 ↔ I ≠ 1 :=
+not_iff_not.mpr coe_ideal_eq_one
 
 end is_fraction_ring
 
@@ -1049,7 +1050,7 @@ variables {R₁}
 
 @[simp] lemma span_finset_eq_zero {ι : Type*} {s : finset ι} {f : ι → K} :
   span_finset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0 :=
-by simp only [← coe_to_submodule_injective.eq_iff, span_finset_coe, coe_zero, submodule.span_eq_bot,
+by simp only [← coe_to_submodule_inj, span_finset_coe, coe_zero, submodule.span_eq_bot,
   set.mem_image, finset.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
 
 lemma span_finset_ne_zero {ι : Type*} {s : finset ι} {f : ι → K} :
@@ -1197,14 +1198,13 @@ lemma mk'_mul_coe_ideal_eq_coe_ideal {I J : ideal R₁} {x y : R₁} (hy : y ∈
   span_singleton R₁⁰ (is_localization.mk' K x ⟨y, hy⟩) * I = (J : fractional_ideal R₁⁰ K) ↔
   ideal.span {x} * I = ideal.span {y} * J :=
 begin
-  have inj : function.injective (coe : ideal R₁ → fractional_ideal R₁⁰ K) := coe_ideal_injective,
   have : span_singleton R₁⁰ (is_localization.mk' _ (1 : R₁) ⟨y, hy⟩) *
            span_singleton R₁⁰ (algebra_map R₁ K y) = 1,
   { rw [span_singleton_mul_span_singleton, mul_comm, ← is_localization.mk'_eq_mul_mk'_one,
         is_localization.mk'_self, span_singleton_one] },
   let y' : (fractional_ideal R₁⁰ K)ˣ := units.mk_of_mul_eq_one _ _ this,
   have coe_y' : ↑y' = span_singleton R₁⁰ (is_localization.mk' K (1 : R₁) ⟨y, hy⟩) := rfl,
-  refine iff.trans _ (y'.mul_right_inj.trans inj.eq_iff),
+  refine iff.trans _ (y'.mul_right_inj.trans coe_ideal_inj),
   rw [coe_y', coe_ideal_mul, coe_ideal_span_singleton, coe_ideal_mul, coe_ideal_span_singleton,
     ←mul_assoc, span_singleton_mul_span_singleton, ←mul_assoc, span_singleton_mul_span_singleton,
     mul_comm (mk' _ _ _), ← is_localization.mk'_eq_mul_mk'_one,
@@ -1323,7 +1323,7 @@ lemma is_noetherian_iff {I : fractional_ideal R₁⁰ K} :
   is_noetherian R₁ I ↔ ∀ J ≤ I, (J : submodule R₁ K).fg :=
 is_noetherian_submodule.trans ⟨λ h J hJ, h _ hJ, λ h J hJ, h ⟨J, is_fractional_of_le hJ⟩ hJ⟩
 
-lemma is_noetherian_coe_to_fractional_ideal [_root_.is_noetherian_ring R₁] (I : ideal R₁) :
+lemma is_noetherian_coe_ideal [_root_.is_noetherian_ring R₁] (I : ideal R₁) :
   is_noetherian R₁ (I : fractional_ideal R₁⁰ K) :=
 begin
   rw is_noetherian_iff,
@@ -1364,7 +1364,7 @@ theorem is_noetherian [_root_.is_noetherian_ring R₁] (I : fractional_ideal R
 begin
   obtain ⟨d, J, h_nzd, rfl⟩ := exists_eq_span_singleton_mul I,
   apply is_noetherian_span_singleton_inv_to_map_mul,
-  apply is_noetherian_coe_to_fractional_ideal,
+  apply is_noetherian_coe_ideal
 end
 
 section adjoin