feat: move the lemma Algebra.coe_norm_int (#8481)

The following lemma: ```lean theorem Algebra.coe_norm_int {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) : Algebra.norm ℤ x = Algebra.norm ℚ (x : K) ``` is currently in `NumberField.Units` but it belongs to `NumberField.Norm`
leanprover-community · Nov 21, 2023 · c40b4df · c40b4df
1 parent 18c15e9
commit c40b4df
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 5 deletions.
diff --git a/Mathlib/NumberTheory/NumberField/Norm.lean b/Mathlib/NumberTheory/NumberField/Norm.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca, Eric Rodriguez
 -/
 import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.RingTheory.Norm
+import Mathlib.RingTheory.Localization.NormTrace
 
 #align_import number_theory.number_field.norm from "leanprover-community/mathlib"@"00f91228655eecdcd3ac97a7fd8dbcb139fe990a"
 
@@ -26,6 +26,14 @@ open scoped NumberField BigOperators
 
 open Finset NumberField Algebra FiniteDimensional
 
+section rat
+
+theorem Algebra.coe_norm_int {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) :
+    Algebra.norm ℤ x = Algebra.norm ℚ (x : K) :=
+  (Algebra.norm_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm
+
+end rat
+
 namespace RingOfIntegers
 
 variable {L : Type*} (K : Type*) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]

diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -55,10 +55,6 @@ theorem Rat.RingOfIntegers.isUnit_iff {x : 𝓞 ℚ} : IsUnit x ↔ (x : ℚ) =
     Subtype.coe_injective.eq_iff]; rfl
 #align rat.ring_of_integers.is_unit_iff Rat.RingOfIntegers.isUnit_iff
 
-theorem Algebra.coe_norm_int {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) :
-    Algebra.norm ℤ x = Algebra.norm ℚ (x : K) :=
-  (Algebra.norm_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm
-
 end Rat
 
 variable (K : Type*) [Field K]