From 2f588be38bb5bec02f218ba14f82fc82eb663f87 Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Mon, 9 Jan 2023 19:56:49 +0000 Subject: [PATCH] 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. --- src/ring_theory/class_group.lean | 21 ++--- .../dedekind_domain/factorization.lean | 2 +- src/ring_theory/dedekind_domain/ideal.lean | 28 +++---- src/ring_theory/fractional_ideal.lean | 82 +++++++++---------- 4 files changed, 61 insertions(+), 72 deletions(-) diff --git a/src/ring_theory/class_group.lean b/src/ring_theory/class_group.lean index 6e894f437902d..cc46021ece831 100644 --- a/src/ring_theory/class_group.lean +++ b/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, diff --git a/src/ring_theory/dedekind_domain/factorization.lean b/src/ring_theory/dedekind_domain/factorization.lean index e2aa140725183..3527aeb7fcd0b 100644 --- a/src/ring_theory/dedekind_domain/factorization.lean +++ b/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 diff --git a/src/ring_theory/dedekind_domain/ideal.lean b/src/ring_theory/dedekind_domain/ideal.lean index 157f23c61278e..a54b392a6011e 100644 --- a/src/ring_theory/dedekind_domain/ideal.lean +++ b/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⟩ diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean index 42cb8547169ec..c17ff5cdfe2bc 100644 --- a/src/ring_theory/fractional_ideal.lean +++ b/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