From d031b37bdb480f21f34d9105c38957358b3aee55 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Tue, 23 Jul 2024 15:36:14 +0100 Subject: [PATCH] build fix --- FltRegular/NumberTheory/Unramified.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean index 588dca0d..6774c071 100644 --- a/FltRegular/NumberTheory/Unramified.lean +++ b/FltRegular/NumberTheory/Unramified.lean @@ -221,7 +221,7 @@ lemma isUnramifiedAt_of_Separable_minpoly' [Algebra.IsSeparable K L] ← Finset.mem_coe, coe_primesOverFinset _ p hpbot] rwa [ne_eq, Ideal.map_eq_bot_iff_of_injective hRS] -lemma isUnramifiedAt_of_Separable_minpoly [IsSeparable K L] +lemma isUnramifiedAt_of_Separable_minpoly [Algebra.IsSeparable K L] (p : Ideal R) [hp : p.IsPrime] (hpbot : p ≠ ⊥) (x : L) (hx : IsIntegral R x) (hx' : Algebra.adjoin K {x} = ⊤) (h : Polynomial.Separable ((minpoly R x).map (Ideal.Quotient.mk p))) :