feat: add Algebra.coe_trace_int (#8513)

From flt-regular.
leanprover-community · Nov 20, 2023 · 7275625 · 7275625
1 parent c21c11f
commit 7275625
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/Mathlib/NumberTheory/NumberField/Norm.lean b/Mathlib/NumberTheory/NumberField/Norm.lean
@@ -26,13 +26,17 @@ open scoped NumberField BigOperators
 
 open Finset NumberField Algebra FiniteDimensional
 
-section rat
+section Rat
 
-theorem Algebra.coe_norm_int {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) :
-    Algebra.norm ℤ x = Algebra.norm ℚ (x : K) :=
+variable {K : Type*} [Field K] [NumberField K] (x : 𝓞 K)
+
+theorem Algebra.coe_norm_int : (Algebra.norm ℤ x : ℚ) = Algebra.norm ℚ (x : K) :=
   (Algebra.norm_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm
 
-end rat
+theorem Algebra.coe_trace_int : (Algebra.trace ℤ _ x : ℚ) = Algebra.trace ℚ K x :=
+  (Algebra.trace_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm
+
+end Rat
 
 namespace RingOfIntegers