build fix

leanprover-community · Jul 23, 2024 · d031b37 · d031b37
1 parent fa4a7fb
commit d031b37
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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))) :