1st commit

Author: xroblot

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

Mathlib/NumberTheory/NumberField/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