From 1fda03db016e1374c9784537459e12efb8fe7664 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 18 Apr 2026 18:06:09 +0800 Subject: [PATCH 1/7] refactor: golf only `ArithmeticFunction/Defs`, `ArithmeticFunction/Zeta` --- .../NumberTheory/ArithmeticFunction/Defs.lean | 26 ++++++------------- .../NumberTheory/ArithmeticFunction/Zeta.lean | 16 +++++------- 2 files changed, 14 insertions(+), 28 deletions(-) diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean index f7387bd07f224d..657cf8dfc035da 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean @@ -262,15 +262,11 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) : theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by ext x - rw [smul_apply] - by_cases x0 : x = 0 - · simp [x0] - have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0] - rw [← sum_subset h] + rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1] · simp - intro y ymem ynotMem - have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff] - simp [y1ne] + · intro d hd hd1 + simp [one_apply_ne hd1] + · simpa using fun hx : x = 0 => by simp [hx] end Module @@ -282,17 +278,11 @@ instance instMonoid : Monoid (ArithmeticFunction R) where one_mul := one_smul' mul_one f := by ext x - rw [mul_apply] - by_cases x0 : x = 0 - · simp [x0] - have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0] - rw [← sum_subset h] + rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1] · simp - intro ⟨y₁, y₂⟩ ymem ynotMem - have y2ne : y₂ ≠ 1 := by - intro con - simp_all - simp [y2ne] + · intro d hd hd1 + simp [one_apply_ne hd1] + · simpa using fun hx : x = 0 => by simp [hx] mul_assoc := mul_smul' instance instSemiring : Semiring (ArithmeticFunction R) where diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean index ab67f48c8097c5..7026d8b0cc6742 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean @@ -78,18 +78,14 @@ theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := coe_zeta_smul_apply -theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : - (f * ζ) x = ∑ i ∈ divisors x, f i := by - rw [mul_apply] - trans ∑ i ∈ divisorsAntidiagonal x, f i.1 - · refine sum_congr rfl fun i hi => ?_ - rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩ - rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one] - · rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk] - theorem coe_zeta_mul_comm [Semiring R] {f : ArithmeticFunction R} : ζ * f = f * ζ := by ext x - rw [coe_zeta_mul_apply, coe_mul_zeta_apply] + rw [mul_apply, ← map_swap_divisorsAntidiagonal, Finset.sum_map] + simp [mul_apply] + +theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : + (f * ζ) x = ∑ i ∈ divisors x, f i := by + rw [← coe_zeta_mul_comm, coe_zeta_mul_apply] theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := by rw [← natCoe_nat ζ, coe_zeta_mul_apply] From c9c59ae0dd10a7b52eacdb2dc4a573b48c4989a5 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 18:20:40 +0800 Subject: [PATCH 2/7] Apply suggestions from code review Co-authored-by: Thomas Browning --- Mathlib/NumberTheory/ArithmeticFunction/Defs.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean index 657cf8dfc035da..36dbeeb0ee7274 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean @@ -260,7 +260,11 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) : apply sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩) (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc) -theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by +theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by + ext x + rw [smul_apply, ← Nat.map_div_right_divisors, sum_map] + simp_rw [Function.Embedding.coeFn_mk, one_apply, ite_smul, one_smul, zero_smul, sum_ite_eq'] + grind [b.map_zero] ext x rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1] · simp @@ -276,7 +280,11 @@ variable [Semiring R] instance instMonoid : Monoid (ArithmeticFunction R) where one_mul := one_smul' - mul_one f := by + mul_one f := by + ext x + rw [mul_apply, ← Nat.map_div_left_divisors, sum_map] + simp_rw [Function.Embedding.coeFn_mk, one_apply, mul_ite, mul_one, mul_zero, sum_ite_eq'] + grind [f.map_zero] ext x rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1] · simp From 61b853b879be32522fe8d874ab06d1b88607a71a Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Sun, 19 Apr 2026 10:21:19 +0000 Subject: [PATCH 3/7] [pre-commit.ci lite] apply automatic fixes --- .../NumberTheory/ArithmeticFunction/Defs.lean | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean index 36dbeeb0ee7274..243bbd0f7cc2a3 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean @@ -260,11 +260,11 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) : apply sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩) (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc) -theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by - ext x - rw [smul_apply, ← Nat.map_div_right_divisors, sum_map] - simp_rw [Function.Embedding.coeFn_mk, one_apply, ite_smul, one_smul, zero_smul, sum_ite_eq'] - grind [b.map_zero] +theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by + ext x + rw [smul_apply, ← Nat.map_div_right_divisors, sum_map] + simp_rw [Function.Embedding.coeFn_mk, one_apply, ite_smul, one_smul, zero_smul, sum_ite_eq'] + grind [b.map_zero] ext x rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1] · simp @@ -280,11 +280,11 @@ variable [Semiring R] instance instMonoid : Monoid (ArithmeticFunction R) where one_mul := one_smul' - mul_one f := by - ext x - rw [mul_apply, ← Nat.map_div_left_divisors, sum_map] - simp_rw [Function.Embedding.coeFn_mk, one_apply, mul_ite, mul_one, mul_zero, sum_ite_eq'] - grind [f.map_zero] + mul_one f := by + ext x + rw [mul_apply, ← Nat.map_div_left_divisors, sum_map] + simp_rw [Function.Embedding.coeFn_mk, one_apply, mul_ite, mul_one, mul_zero, sum_ite_eq'] + grind [f.map_zero] ext x rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1] · simp From f989e7e44b174b6964bfc9ff247d823fa6ed852d Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 18:22:35 +0800 Subject: [PATCH 4/7] Update Defs.lean --- .../NumberTheory/ArithmeticFunction/Defs.lean | 34 ++++++++++--------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean index 243bbd0f7cc2a3..f7387bd07f224d 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean @@ -262,15 +262,15 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) : theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by ext x - rw [smul_apply, ← Nat.map_div_right_divisors, sum_map] - simp_rw [Function.Embedding.coeFn_mk, one_apply, ite_smul, one_smul, zero_smul, sum_ite_eq'] - grind [b.map_zero] - ext x - rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1] + rw [smul_apply] + by_cases x0 : x = 0 + · simp [x0] + have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0] + rw [← sum_subset h] · simp - · intro d hd hd1 - simp [one_apply_ne hd1] - · simpa using fun hx : x = 0 => by simp [hx] + intro y ymem ynotMem + have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff] + simp [y1ne] end Module @@ -282,15 +282,17 @@ instance instMonoid : Monoid (ArithmeticFunction R) where one_mul := one_smul' mul_one f := by ext x - rw [mul_apply, ← Nat.map_div_left_divisors, sum_map] - simp_rw [Function.Embedding.coeFn_mk, one_apply, mul_ite, mul_one, mul_zero, sum_ite_eq'] - grind [f.map_zero] - ext x - rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1] + rw [mul_apply] + by_cases x0 : x = 0 + · simp [x0] + have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0] + rw [← sum_subset h] · simp - · intro d hd hd1 - simp [one_apply_ne hd1] - · simpa using fun hx : x = 0 => by simp [hx] + intro ⟨y₁, y₂⟩ ymem ynotMem + have y2ne : y₂ ≠ 1 := by + intro con + simp_all + simp [y2ne] mul_assoc := mul_smul' instance instSemiring : Semiring (ArithmeticFunction R) where From c425ccd6b2764fc2e7dc86f9f8a2f6c7696d515e Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 18:26:45 +0800 Subject: [PATCH 5/7] add file --- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 72 +++++++++------------- 1 file changed, 30 insertions(+), 42 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index f4861f75d916b5..603fb8b7c55d69 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -549,42 +549,24 @@ theorem nonempty_algEquiv_adjoin_of_isSepClosed [IsCyclotomicExtension S K L] have := isSeparable S K L let i : L →ₐ[K] M := IsSepClosed.lift refine ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans - (IntermediateField.equivOfEq (le_antisymm ?_ ?_))⟩ - · rintro x (hx : x ∈ i.range) - let e := Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_›).2 - |>.trans Subalgebra.topEquiv - have hrange : i.range = (i.comp (AlgHomClass.toAlgHom e)).range := by - ext x - simp only [AlgHom.mem_range, AlgHom.coe_comp, AlgHom.coe_coe, Function.comp_apply] - constructor - · rintro ⟨y, rfl⟩; exact ⟨e.symm y, by simp⟩ - · rintro ⟨y, rfl⟩; exact ⟨e y, rfl⟩ - rw [hrange, AlgHom.mem_range] at hx - obtain ⟨⟨y, hy⟩, rfl⟩ := hx - induction hy using Algebra.adjoin_induction with - | mem x hx => - obtain ⟨n, hn, h1, h2⟩ := hx - apply IntermediateField.subset_adjoin - use n, hn, h1 - rw [← map_pow, ← map_one (i.comp (AlgHomClass.toAlgHom e))] - congr 1 - apply_fun _ using Subtype.val_injective - simpa - | algebraMap x => - convert IntermediateField.algebraMap_mem _ x - exact AlgHom.commutes _ x - | add x y hx hy ihx ihy => - convert add_mem ihx ihy - exact map_add (i.comp (AlgHomClass.toAlgHom e)) ⟨x, hx⟩ ⟨y, hy⟩ - | mul x y hx hy ihx ihy => - convert mul_mem ihx ihy - exact map_mul (i.comp (AlgHomClass.toAlgHom e)) ⟨x, hx⟩ ⟨y, hy⟩ - · rw [IntermediateField.adjoin_le_iff] - rintro x ⟨n, hn, h1, h2⟩ - have := NeZero.mk h1 + (IntermediateField.equivOfEq ?_)⟩ + rw [AlgHom.fieldRange_eq_map] + have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ := by + exact IntermediateField.adjoin_eq_top_of_algebra (F := K) + (S := {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) + (((IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_›).2) + rw [← htop, IntermediateField.adjoin_map] + apply le_antisymm <;> rw [IntermediateField.adjoin_le_iff] + · rintro _ ⟨y, ⟨n, hn, h1, h2⟩, rfl⟩ + exact IntermediateField.subset_adjoin (F := K) + (S := {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⟨n, hn, h1, by + simpa using congrArg i h2⟩ + · rintro x ⟨n, hn, h1, h2⟩ + have : NeZero n := ⟨h1⟩ obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1 obtain ⟨m, -, rfl⟩ := (hy.map_of_injective (f := i) i.injective).eq_pow_of_pow_eq_one h2 - exact ⟨y ^ m, by simp⟩ + exact pow_mem (IntermediateField.subset_adjoin (F := K) + (S := i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m theorem isGalois [IsCyclotomicExtension S K L] : IsGalois K L := by rw [isGalois_iff] @@ -681,14 +663,8 @@ deriving Field, Inhabited namespace CyclotomicField -variable [Algebra A K] in -deriving instance Algebra A, IsScalarTower A K for CyclotomicField n K - -instance algebra : Algebra K (CyclotomicField n K) := inferInstance - -/-- Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -/ -example : Ring.toIntAlgebra (CyclotomicField n ℚ) = CyclotomicField.instAlgebra _ _ _ := rfl - +instance algebra : Algebra K (CyclotomicField n K) := + inferInstanceAs <| Algebra K (cyclotomic n K).SplittingField instance [CharZero K] : CharZero (CyclotomicField n K) := charZero_of_injective_algebraMap (algebraMap K _).injective @@ -740,6 +716,17 @@ variable [Algebra A K] section CyclotomicRing +/-- If `K` is an `A`-algebra, the `A`-algebra structure on `CyclotomicField n K`. +-/ +instance CyclotomicField.algebraBase : Algebra A (CyclotomicField n K) := + SplittingField.instAlgebra (cyclotomic n K) + +/-- Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -/ +example : Ring.toIntAlgebra (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ := rfl + +instance {R : Type*} [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicField n K) := + SplittingField.instIsScalarTower _ + instance [IsDomain A] [IsFractionRing A K] : Module.IsTorsionFree A (CyclotomicField n K) := by rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K (CyclotomicField n K)] @@ -814,6 +801,7 @@ instance isCyclotomicExtension [IsDomain A] [IsFractionRing A K] [NeZero ((n : · exact Subalgebra.add_mem _ hy hz · exact Subalgebra.mul_mem _ hy hz +set_option backward.isDefEq.respectTransparency false in instance [IsFractionRing A K] [IsDomain A] [NeZero (n : A)] : IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K) where map_units := fun ⟨x, hx⟩ => by From 14ce33e36d9a8154af7e017e8cca39452a78c01c Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 18:38:29 +0800 Subject: [PATCH 6/7] add file --- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 38 ++++++++-------------- 1 file changed, 14 insertions(+), 24 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 603fb8b7c55d69..ce83dc329594f0 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -551,22 +551,18 @@ theorem nonempty_algEquiv_adjoin_of_isSepClosed [IsCyclotomicExtension S K L] refine ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans (IntermediateField.equivOfEq ?_)⟩ rw [AlgHom.fieldRange_eq_map] - have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ := by - exact IntermediateField.adjoin_eq_top_of_algebra (F := K) - (S := {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) - (((IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_›).2) + have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ := + IntermediateField.adjoin_eq_top_of_algebra K _ ((iff_adjoin_eq_top S K L).1 ‹_›).2 rw [← htop, IntermediateField.adjoin_map] apply le_antisymm <;> rw [IntermediateField.adjoin_le_iff] · rintro _ ⟨y, ⟨n, hn, h1, h2⟩, rfl⟩ - exact IntermediateField.subset_adjoin (F := K) - (S := {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⟨n, hn, h1, by - simpa using congrArg i h2⟩ + exact IntermediateField.subset_adjoin K _ ⟨n, hn, h1, by simpa using congrArg i h2⟩ · rintro x ⟨n, hn, h1, h2⟩ have : NeZero n := ⟨h1⟩ obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1 - obtain ⟨m, -, rfl⟩ := (hy.map_of_injective (f := i) i.injective).eq_pow_of_pow_eq_one h2 - exact pow_mem (IntermediateField.subset_adjoin (F := K) - (S := i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m + obtain ⟨m, -, rfl⟩ := (hy.map_of_injective i.injective).eq_pow_of_pow_eq_one h2 + exact pow_mem (IntermediateField.subset_adjoin K (i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) + ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m theorem isGalois [IsCyclotomicExtension S K L] : IsGalois K L := by rw [isGalois_iff] @@ -663,8 +659,14 @@ deriving Field, Inhabited namespace CyclotomicField -instance algebra : Algebra K (CyclotomicField n K) := - inferInstanceAs <| Algebra K (cyclotomic n K).SplittingField +variable [Algebra A K] in +deriving instance Algebra A, IsScalarTower A K for CyclotomicField n K + +instance algebra : Algebra K (CyclotomicField n K) := inferInstance + +/-- Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -/ +example : Ring.toIntAlgebra (CyclotomicField n ℚ) = CyclotomicField.instAlgebra _ _ _ := rfl + instance [CharZero K] : CharZero (CyclotomicField n K) := charZero_of_injective_algebraMap (algebraMap K _).injective @@ -716,17 +718,6 @@ variable [Algebra A K] section CyclotomicRing -/-- If `K` is an `A`-algebra, the `A`-algebra structure on `CyclotomicField n K`. --/ -instance CyclotomicField.algebraBase : Algebra A (CyclotomicField n K) := - SplittingField.instAlgebra (cyclotomic n K) - -/-- Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -/ -example : Ring.toIntAlgebra (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ := rfl - -instance {R : Type*} [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicField n K) := - SplittingField.instIsScalarTower _ - instance [IsDomain A] [IsFractionRing A K] : Module.IsTorsionFree A (CyclotomicField n K) := by rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K (CyclotomicField n K)] @@ -801,7 +792,6 @@ instance isCyclotomicExtension [IsDomain A] [IsFractionRing A K] [NeZero ((n : · exact Subalgebra.add_mem _ hy hz · exact Subalgebra.mul_mem _ hy hz -set_option backward.isDefEq.respectTransparency false in instance [IsFractionRing A K] [IsDomain A] [NeZero (n : A)] : IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K) where map_units := fun ⟨x, hx⟩ => by From c3eeaa1cb1290367f6b74f812e63d9378ceb45ce Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 18:41:03 +0800 Subject: [PATCH 7/7] add file --- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index ce83dc329594f0..64f9a5cb00b6d5 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -550,10 +550,9 @@ theorem nonempty_algEquiv_adjoin_of_isSepClosed [IsCyclotomicExtension S K L] let i : L →ₐ[K] M := IsSepClosed.lift refine ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans (IntermediateField.equivOfEq ?_)⟩ - rw [AlgHom.fieldRange_eq_map] have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ := IntermediateField.adjoin_eq_top_of_algebra K _ ((iff_adjoin_eq_top S K L).1 ‹_›).2 - rw [← htop, IntermediateField.adjoin_map] + rw [AlgHom.fieldRange_eq_map, ← htop, IntermediateField.adjoin_map] apply le_antisymm <;> rw [IntermediateField.adjoin_le_iff] · rintro _ ⟨y, ⟨n, hn, h1, h2⟩, rfl⟩ exact IntermediateField.subset_adjoin K _ ⟨n, hn, h1, by simpa using congrArg i h2⟩