From 7f79ab64c128abce426503c2f04ff864c87e923e Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 25 Oct 2024 14:11:13 +0200 Subject: [PATCH] better --- FltRegular/NumberTheory/Different.lean | 7 ++++++- FltRegular/NumberTheory/KummersLemma/Field.lean | 2 +- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index 45c96014..9e9f1b0f 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/FltRegular/NumberTheory/Different.lean @@ -1,6 +1,5 @@ import Mathlib.RingTheory.DedekindDomain.Different import Mathlib.RingTheory.DedekindDomain.Ideal -import Mathlib.RingTheory.DedekindDomain.Different import Mathlib.RingTheory.Localization.FractionRing import Mathlib.RingTheory.Trace.Quotient import Mathlib.NumberTheory.KummerDedekind @@ -36,6 +35,12 @@ open nonZeroDivisors IsLocalization Matrix Algebra variable [IsDedekindDomain B] +noncomputable +example : InvolutiveInv (FractionalIdeal B⁰ L) := by + exact DivisionMonoid.toInvolutiveInv + +#synth DivisionMonoid (FractionalIdeal B⁰ L) + include K L in lemma pow_sub_one_dvd_differentIdeal_aux [IsDedekindDomain A] [NoZeroSMulDivisors A B] [Module.Finite A B] diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 25d8e04d..d4229a6f 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -272,7 +272,7 @@ lemma separable_poly (I : Ideal (𝓞 K)) [I.IsMaximal] : rw [ne_eq, Ideal.map_eq_top_iff]; exact Ideal.IsMaximal.ne_top ‹_› · intros x y e; ext; exact (algebraMap K L).injective (congr_arg Subtype.val e) · intros x; exact IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ L x) - rw [← Polynomial.separable_map i, map_map, Ideal.quotientMap_comp_mk, ← map_map] + rw [← Polynomial.separable_map' i, map_map, Ideal.quotientMap_comp_mk, ← map_map] apply Separable.map apply separable_poly_aux hp hζ u hcong exact root_X_pow_sub_C_pow _ _