From 2c17fb466945b4bd2191cd00e046979d820adfea Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sat, 19 Oct 2024 23:44:28 +0000 Subject: [PATCH] fix moved import --- Mathlib/SetTheory/Cardinal/FieldEmb.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/FieldEmb.lean b/Mathlib/SetTheory/Cardinal/FieldEmb.lean index 477ef20485049..a6e7fd31d303f 100644 --- a/Mathlib/SetTheory/Cardinal/FieldEmb.lean +++ b/Mathlib/SetTheory/Cardinal/FieldEmb.lean @@ -3,10 +3,10 @@ Copyright (c) 2024 Junyan Xu. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Junyan Xu -/ -import Mathlib.Data.Set.Intervals.WithBotTop import Mathlib.FieldTheory.MvPolynomial import Mathlib.FieldTheory.SeparableClosure import Mathlib.FieldTheory.PurelyInseparable +import Mathlib.Order.Interval.Set.WithBotTop /-! # Number of embeddings of an infinite algebraic field extension into the algebraic closure