From 663eb7383a61ff00e4f1a4e9668cbdaa21f97fba Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Mon, 20 Apr 2026 17:07:36 +0800 Subject: [PATCH 1/2] refactor(NumberTheory): golf Cyclotomic.Basic --- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 50 +++++++--------------- 1 file changed, 16 insertions(+), 34 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index f4861f75d916b5..fb188d33d9d298 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] From a6d60832e953d5e4648227484ae0ed7c50f9c061 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 20 Apr 2026 17:38:46 +0800 Subject: [PATCH 2/2] Update Basic.lean --- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index fb188d33d9d298..64f9a5cb00b6d5 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -550,23 +550,18 @@ 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} = ⊤ := 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] + 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 [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 (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]