Skip to content

Commit

Permalink
fix moved import
Browse files Browse the repository at this point in the history
  • Loading branch information
alreadydone committed Oct 19, 2024
1 parent 6479159 commit 2c17fb4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/SetTheory/Cardinal/FieldEmb.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 2c17fb4

Please sign in to comment.