ops

leanprover-community · Oct 25, 2024 · 33953c1 · 33953c1
1 parent 7f79ab6
commit 33953c1
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 7 deletions.
diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean
@@ -35,12 +35,6 @@ 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
@@ -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 _ _