From 8418eab4284ceb8b3ddf2958089661974c8e5847 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 10:00:48 +0800 Subject: [PATCH 1/2] refactor(NumberTheory): golf Cyclotomic/Gal --- Mathlib/NumberTheory/Cyclotomic/Gal.lean | 22 ++++------------------ 1 file changed, 4 insertions(+), 18 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Gal.lean b/Mathlib/NumberTheory/Cyclotomic/Gal.lean index 4fa73cdc884f22..6fc270613b9202 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Gal.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Gal.lean @@ -56,24 +56,10 @@ variable [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] field extension. -/ theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by intro f g hfg - apply_fun Units.val at hfg - simp only [IsPrimitiveRoot.coe_autToPow_apply] at hfg - generalize_proofs hf' hg' at hfg - have hf := hf'.choose_spec - have hg := hg'.choose_spec - generalize_proofs hζ at hf hg - suffices f (hμ.toRootsOfUnity : Lˣ) = g (hμ.toRootsOfUnity : Lˣ) by - apply AlgEquiv.coe_algHom_injective - apply (hμ.powerBasis K).algHom_ext - exact this - rw [ZMod.natCast_eq_natCast_iff] at hfg - refine (hf.trans ?_).trans hg.symm - rw [← rootsOfUnity.coe_pow _ hf'.choose, ← rootsOfUnity.coe_pow _ hg'.choose] - congr 2 - rw [pow_eq_pow_iff_modEq] - convert hfg - conv => enter [2]; rw [hμ.eq_orderOf, ← hμ.val_toRootsOfUnity_coe] - rw [orderOf_units, Subgroup.orderOf_coe] + apply AlgEquiv.coe_algHom_injective + apply (hμ.powerBasis K).algHom_ext + simpa only [IsPrimitiveRoot.autToPow_spec] using + congrArg (fun t : (ZMod n)ˣ ↦ μ ^ (t : ZMod n).val) hfg end IsPrimitiveRoot From a0b8d518f3a2556f59d5e0e494feec224dba394d Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 26 Apr 2026 21:47:04 +0800 Subject: [PATCH 2/2] avoid defeq abuse --- Mathlib/NumberTheory/Cyclotomic/Gal.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Gal.lean b/Mathlib/NumberTheory/Cyclotomic/Gal.lean index 6fc270613b9202..2c186a7b95544f 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Gal.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Gal.lean @@ -56,10 +56,11 @@ variable [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] field extension. -/ theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by intro f g hfg - apply AlgEquiv.coe_algHom_injective - apply (hμ.powerBasis K).algHom_ext - simpa only [IsPrimitiveRoot.autToPow_spec] using - congrArg (fun t : (ZMod n)ˣ ↦ μ ^ (t : ZMod n).val) hfg + have : f.toAlgHom = g.toAlgHom := by + apply (hμ.powerBasis K).algHom_ext + rw [AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe, AlgHom.coe_coe, + powerBasis_gen, ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg] + exact AlgEquiv.coe_algHom_injective this end IsPrimitiveRoot