diff --git a/Mathlib.lean b/Mathlib.lean
index 091ae6b05a7371..80f5aec6470381 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2494,7 +2494,6 @@ import Mathlib.NumberTheory.Multiplicity
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
 import Mathlib.NumberTheory.NumberField.ClassNumber
-import Mathlib.NumberTheory.NumberField.Discriminant
 import Mathlib.NumberTheory.NumberField.Embeddings
 import Mathlib.NumberTheory.NumberField.Norm
 import Mathlib.NumberTheory.NumberField.Units
diff --git a/Mathlib/NumberTheory/NumberField/Discriminant.lean b/Mathlib/NumberTheory/NumberField/Discriminant.lean
deleted file mode 100644
index b3c79c7017c55b..00000000000000
--- a/Mathlib/NumberTheory/NumberField/Discriminant.lean
+++ /dev/null
@@ -1,57 +0,0 @@
-/-
-Copyright (c) 2023 Xavier Roblot. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Xavier Roblot
--/
-import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.RingTheory.Localization.NormTrace
-
-/-!
-# Number field discriminant
-This file defines the discrimiant of a number field.
-
--/
-
-namespace NumberField
-
-open NumberField Matrix
-
-variable (K : Type _) [Field K] [NumberField K]
-
-/-- The discriminant of a number field. -/
-noncomputable def discr : ℤ := Algebra.discr ℤ (RingOfIntegers.basis K)
-
-theorem coe_discr : (discr K : ℚ) = Algebra.discr ℚ (integralBasis K) := by
-  rw [discr]
-  exact (Algebra.discr_localizationLocalization ℤ _ K (RingOfIntegers.basis K)).symm
-
-theorem discr_ne_zero : discr K ≠ 0 := by
-  rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]
-  exact Algebra.discr_not_zero_of_basis ℚ (integralBasis K)
-
-theorem discr_eq_discr {ι : Type _} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ (𝓞 K)) :
-    Algebra.discr ℤ b = discr K := by
-  let b₀ := Basis.reindex (RingOfIntegers.basis K) (Basis.indexEquiv (RingOfIntegers.basis K) b)
-  rw [Algebra.discr_eq_discr (𝓞 K) b b₀, discr, Basis.coe_reindex, Algebra.discr_reindex]
-
-end NumberField
-
-namespace Rat
-
-open NumberField
-
-theorem discr : discr ℚ = 1 := by
-  let b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
-    Basis.map (Basis.singleton (Fin 1) ℤ) ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
-  calc NumberField.discr ℚ
-    _ = Algebra.discr ℤ b := by convert (discr_eq_discr ℚ b).symm
-    _ = Matrix.det (Algebra.traceMatrix ℤ b) := rfl
-    _ = Algebra.trace ℤ (𝓞 ℚ) 1 := ?_
-    _ = 1                 := by rw [Algebra.trace_eq_matrix_trace b]; norm_num
-  rw [Matrix.det_unique, Algebra.traceMatrix_apply, Basis.map_apply, Basis.singleton_apply,
-    AddEquiv.toIntLinearEquiv_symm, AddEquiv.coe_toIntLinearEquiv, RingEquiv.toAddEquiv_eq_coe,
-    show (AddEquiv.symm ringOfIntegersEquiv) (1 : ℤ) = (1 : 𝓞 ℚ) by
-      rw [AddEquiv.symm_apply_eq, RingEquiv.coe_toAddEquiv, map_one],
-    Algebra.traceForm_apply, mul_one]
-
-end Rat
diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean
index c751bf10c80755..a0a08e4d5b3c6f 100644
--- a/Mathlib/RingTheory/Discriminant.lean
+++ b/Mathlib/RingTheory/Discriminant.lean
@@ -3,9 +3,9 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
-import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.Trace
 import Mathlib.RingTheory.Norm
+import Mathlib.NumberTheory.NumberField.Basic
 
 #align_import ring_theory.discriminant from "leanprover-community/mathlib"@"3e068ece210655b7b9a9477c3aff38a492400aa1"
 
@@ -376,21 +376,6 @@ end Integral
 
 end Field
 
-section Int
-
-end Int
-
-/-- Two (finite) ℤ-basis have the same discriminant. -/
-theorem discr_eq_discr [Fintype ι] (b : Basis ι ℤ A) (b' : Basis ι ℤ A) :
-    Algebra.discr ℤ b = Algebra.discr ℤ b' := by
-  convert Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)
-  · rw [Basis.toMatrix_map_vecMul]
-  · suffices IsUnit (b'.toMatrix b).det by
-      rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
-      rw [this, one_mul]
-    rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']
-    exact LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'
-
 end Discr
 
 end Algebra