From 17f3e5d81e729be86e3539613710a16a05f1c698 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 28 May 2026 18:11:31 +0100 Subject: [PATCH 01/12] add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime --- Mathlib/RingTheory/ClassGroup.lean | 37 ++++++++++++++++++++++++++---- 1 file changed, 33 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index 53c4d81062fa4d..01e262db5744dc 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -140,7 +140,7 @@ theorem ClassGroup.mk_eq_mk_of_coe_ideal {I J : (FractionalIdeal R⁰ <| Fractio simpa only [isUnit_iff_ne_zero, ne_eq, mk'_eq_zero_iff_eq_zero] using hx refine ⟨this.unit, ?_⟩ rw [mul_comm, ← Units.val_inj, Units.val_mul, coe_toPrincipalIdeal] - convert! + convert (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h theorem ClassGroup.mk_eq_one_of_coe_ideal {I : (FractionalIdeal R⁰ <| FractionRing R)ˣ} @@ -222,8 +222,6 @@ theorem ClassGroup.mk_canonicalEquiv (K' : Type*) [Field K'] [Algebra R K'] [IsF ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans, FractionalIdeal.canonicalEquiv_trans_canonicalEquiv] -set_option linter.overlappingInstances false - /-- Send a nonzero integral ideal to an invertible fractional ideal. -/ def FractionalIdeal.mk0 [IsDedekindDomain R] : (Ideal R)⁰ →* (FractionalIdeal R⁰ K)ˣ where @@ -356,6 +354,21 @@ theorem ClassGroup.mk_eq_one_iff {I : (FractionalIdeal R⁰ K)ˣ} : · intro x_eq; apply Units.ne_zero I; simp [hx', x_eq] · simp [hx'] +/-- A fractional ideal is principal if a power coprime to the class number is principal. -/ +theorem FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] + [Fintype (ClassGroup R)] {n : ℕ} (hn : n.Coprime (Fintype.card (ClassGroup R))) + (I : FractionalIdeal R⁰ K) (hI : ((I ^ n : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal) : + (I : Submodule R K).IsPrincipal := by + by_cases hI0 : I = 0 + · rw [hI0, FractionalIdeal.coe_zero] + exact bot_isPrincipal + rw [← Ne, ← isUnit_iff_ne_zero] at hI0 + change Submodule.IsPrincipal ((hI0.unit' : FractionalIdeal R⁰ K) : Submodule R K) + rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] + refine ⟨?_, orderOf_dvd_card⟩ + rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff] + simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI] + /-- If the class group is trivial, any unit fractional ideal is principal. -/ theorem ClassGroup.isPrincipal_coeSubmodule_of_isUnit [Subsingleton (ClassGroup R)] (I : FractionalIdeal R⁰ K) (hI : IsUnit I) : @@ -378,6 +391,22 @@ theorem ClassGroup.mk0_eq_one_iff [IsDedekindDomain R] {I : Ideal R} (hI : I ∈ ClassGroup.mk0 ⟨I, hI⟩ = 1 ↔ I.IsPrincipal := ClassGroup.mk_eq_one_iff.trans (coeSubmodule_isPrincipal R _) +/-- An ideal is principal if a power coprime to the class number is principal. -/ +theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] + [Fintype (ClassGroup R)] {n : ℕ} (hn : n.Coprime (Fintype.card (ClassGroup R))) + {I : Ideal R} (hI : (I ^ n).IsPrincipal) : I.IsPrincipal := by + by_cases hI0 : I = 0 + · rw [hI0] + exact bot_isPrincipal + rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero _)] at hI ⊢ + swap + · exact hI0 + swap + · exact pow_ne_zero n hI0 + · rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] + refine ⟨?_, orderOf_dvd_card⟩ + rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow] + theorem ClassGroup.mk0_eq_mk0_inv_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} : ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔ ∃ x ≠ (0 : R), I * J = Ideal.span {x} := by @@ -410,7 +439,7 @@ theorem card_classGroup_eq_one [IsPrincipalIdealRing R] : Fintype.card (ClassGro /-- The class number is `1` iff the ring of integers is a principal ideal domain. -/ theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)] : Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R := by - constructor; swap; · intros; convert! card_classGroup_eq_one (R := R) + constructor; swap; · intros; convert card_classGroup_eq_one (R := R) rw [Fintype.card_eq_one_iff] rintro ⟨I, hI⟩ have eq_one : ∀ J : ClassGroup R, J = 1 := fun J => (hI J).trans (hI 1).symm From 7a9347fc04b46ca48cece9d0dd1efac85f77d546 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 28 May 2026 19:07:46 +0100 Subject: [PATCH 02/12] let's keep this --- Mathlib/RingTheory/ClassGroup.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index 01e262db5744dc..31310ee5b56919 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -140,7 +140,7 @@ theorem ClassGroup.mk_eq_mk_of_coe_ideal {I J : (FractionalIdeal R⁰ <| Fractio simpa only [isUnit_iff_ne_zero, ne_eq, mk'_eq_zero_iff_eq_zero] using hx refine ⟨this.unit, ?_⟩ rw [mul_comm, ← Units.val_inj, Units.val_mul, coe_toPrincipalIdeal] - convert + convert! (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h theorem ClassGroup.mk_eq_one_of_coe_ideal {I : (FractionalIdeal R⁰ <| FractionRing R)ˣ} From 44021cf0f65dbdc06b3f0c5f5a8e16c23c1faa67 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 28 May 2026 19:15:45 +0100 Subject: [PATCH 03/12] ops --- Mathlib/RingTheory/ClassGroup.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index 31310ee5b56919..96c03b6ebac19e 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -222,6 +222,8 @@ theorem ClassGroup.mk_canonicalEquiv (K' : Type*) [Field K'] [Algebra R K'] [IsF ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans, FractionalIdeal.canonicalEquiv_trans_canonicalEquiv] +set_option linter.overlappingInstances false + /-- Send a nonzero integral ideal to an invertible fractional ideal. -/ def FractionalIdeal.mk0 [IsDedekindDomain R] : (Ideal R)⁰ →* (FractionalIdeal R⁰ K)ˣ where @@ -439,7 +441,7 @@ theorem card_classGroup_eq_one [IsPrincipalIdealRing R] : Fintype.card (ClassGro /-- The class number is `1` iff the ring of integers is a principal ideal domain. -/ theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)] : Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R := by - constructor; swap; · intros; convert card_classGroup_eq_one (R := R) + constructor; swap; · intros; convert! card_classGroup_eq_one (R := R) rw [Fintype.card_eq_one_iff] rintro ⟨I, hI⟩ have eq_one : ∀ J : ClassGroup R, J = 1 := fun J => (hI J).trans (hI 1).symm From f874c1a7aad82d3213d3a2269dfec2b24b581a27 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 25 Jun 2026 11:39:25 +0200 Subject: [PATCH 04/12] Update Mathlib/RingTheory/ClassGroup/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com> --- Mathlib/RingTheory/ClassGroup/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index eff0d15086f389..bd0438f6707725 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -371,8 +371,7 @@ theorem FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDom (I : FractionalIdeal R⁰ K) (hI : ((I ^ n : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal) : (I : Submodule R K).IsPrincipal := by by_cases hI0 : I = 0 - · rw [hI0, FractionalIdeal.coe_zero] - exact bot_isPrincipal + · simp [hI0, bot_isPrincipal] rw [← Ne, ← isUnit_iff_ne_zero] at hI0 change Submodule.IsPrincipal ((hI0.unit' : FractionalIdeal R⁰ K) : Submodule R K) rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] From 1ce48bf8ecfe72244f910635d57baab20d2c3139 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 25 Jun 2026 11:39:35 +0200 Subject: [PATCH 05/12] Update Mathlib/RingTheory/ClassGroup/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com> --- Mathlib/RingTheory/ClassGroup/Basic.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index bd0438f6707725..19feb5a725e260 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -408,12 +408,9 @@ theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] by_cases hI0 : I = 0 · rw [hI0] exact bot_isPrincipal - rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero _)] at hI ⊢ - swap - · exact hI0 - swap - · exact pow_ne_zero n hI0 - · rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] + rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero (pow_ne_zero n hI0))] at hI + rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero hI0), ← orderOf_eq_one_iff, + ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩ rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow] From 5254ad6b174917a25512056fa9f3269fe5a06523 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 25 Jun 2026 11:39:44 +0200 Subject: [PATCH 06/12] Update Mathlib/RingTheory/ClassGroup/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com> --- Mathlib/RingTheory/ClassGroup/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index 19feb5a725e260..2d056a35900962 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -406,8 +406,7 @@ theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] [Fintype (ClassGroup R)] {n : ℕ} (hn : n.Coprime (Fintype.card (ClassGroup R))) {I : Ideal R} (hI : (I ^ n).IsPrincipal) : I.IsPrincipal := by by_cases hI0 : I = 0 - · rw [hI0] - exact bot_isPrincipal + · simp [hI0, bot_isPrincipal] rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero (pow_ne_zero n hI0))] at hI rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero hI0), ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] From e401f74c7d062bcebfc76ee211bc1a0645dbaebb Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Thu, 25 Jun 2026 09:40:34 +0000 Subject: [PATCH 07/12] [pre-commit.ci lite] apply automatic fixes --- Mathlib/RingTheory/ClassGroup/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index 2d056a35900962..2f829dac6e5f2b 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -408,7 +408,7 @@ theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] by_cases hI0 : I = 0 · simp [hI0, bot_isPrincipal] rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero (pow_ne_zero n hI0))] at hI - rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero hI0), ← orderOf_eq_one_iff, + rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero hI0), ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩ rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow] From 20ee7d8ab5d8659b93d16c4643c88ca86623095f Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 25 Jun 2026 12:04:19 +0200 Subject: [PATCH 08/12] fix --- Mathlib/RingTheory/ClassGroup/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index 2f829dac6e5f2b..084cc39d931126 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -410,8 +410,8 @@ theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero (pow_ne_zero n hI0))] at hI rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero hI0), ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] - refine ⟨?_, orderOf_dvd_card⟩ - rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow] + refine ⟨?_, orderOf_dvd_card⟩ + rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow] theorem ClassGroup.mk0_eq_mk0_inv_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} : ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔ From 8cc378d838bf5724527803303ddab5f6637be872 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 21 Jul 2026 10:03:44 +0800 Subject: [PATCH 09/12] Update Mathlib/RingTheory/ClassGroup/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com> --- Mathlib/RingTheory/ClassGroup/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index 084cc39d931126..d9bd8f847f32df 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -373,8 +373,8 @@ theorem FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDom by_cases hI0 : I = 0 · simp [hI0, bot_isPrincipal] rw [← Ne, ← isUnit_iff_ne_zero] at hI0 - change Submodule.IsPrincipal ((hI0.unit' : FractionalIdeal R⁰ K) : Submodule R K) - rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] +rw [← hI0.val_unit', ← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, + Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩ rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff] simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI] From 9e26a0ddfdeb8f92def17d2a1c8b83c73ba5a6c1 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 21 Jul 2026 10:58:42 +0800 Subject: [PATCH 10/12] fix --- Mathlib/RingTheory/ClassGroup/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index d9bd8f847f32df..3220c695d035fe 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -373,7 +373,7 @@ theorem FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDom by_cases hI0 : I = 0 · simp [hI0, bot_isPrincipal] rw [← Ne, ← isUnit_iff_ne_zero] at hI0 -rw [← hI0.val_unit', ← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, + rw [← hI0.val_unit', ← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩ rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff] From b2a4aaa4235be5c06845f50a2db6d28bb8da3b90 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 23 Jul 2026 13:18:16 +0800 Subject: [PATCH 11/12] Update Mathlib/RingTheory/ClassGroup/Basic.lean Co-authored-by: Anne Baanen --- Mathlib/RingTheory/ClassGroup/Basic.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index 1bab391141cd9f..5d5975f4471421 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -370,14 +370,13 @@ theorem FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDom [Fintype (ClassGroup R)] {n : ℕ} (hn : n.Coprime (Fintype.card (ClassGroup R))) (I : FractionalIdeal R⁰ K) (hI : ((I ^ n : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal) : (I : Submodule R K).IsPrincipal := by - by_cases hI0 : I = 0 - · simp [hI0, bot_isPrincipal] - rw [← Ne, ← isUnit_iff_ne_zero] at hI0 - rw [← hI0.val_unit', ← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, + obtain (rfl | ⟨u, rfl⟩) := GroupWithZero.eq_zero_or_unit I + · simp [bot_isPrincipal] + rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩ rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff] - simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI] + exact_mod_cast hI /-- If the class group is trivial, any unit fractional ideal is principal. -/ theorem ClassGroup.isPrincipal_coeSubmodule_of_isUnit [Subsingleton (ClassGroup R)] From ddc770be569b0701aabcaa413c89e2579cf5060b Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 23 Jul 2026 13:18:26 +0800 Subject: [PATCH 12/12] Update Mathlib/RingTheory/ClassGroup/Basic.lean Co-authored-by: Anne Baanen --- Mathlib/RingTheory/ClassGroup/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index 5d5975f4471421..e91fe290266922 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -406,7 +406,7 @@ theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime [IsDedekindDomain R] {I : Ideal R} (hI : (I ^ n).IsPrincipal) : I.IsPrincipal := by by_cases hI0 : I = 0 · simp [hI0, bot_isPrincipal] - rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero (pow_ne_zero n hI0))] at hI + rw [← ClassGroup.mk0_eq_one_iff (pow_mem (mem_nonZeroDivisors_of_ne_zero hI0) n)] at hI rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero hI0), ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn, Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩