Merge branch 'main' into bump_to_v4.16.0-rc1

ImperialCollegeLondon · Jan 6, 2025 · 0a4af71 · 0a4af71
2 parents 6608605 + 844227a
commit 0a4af71
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/FLT/Mathlib/NumberTheory/NumberField/Basic.lean b/FLT/Mathlib/NumberTheory/NumberField/Basic.lean
@@ -0,0 +1,7 @@
+import Mathlib.NumberTheory.NumberField.Basic
+
+open scoped NumberField
+
+theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) :
+    (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
+  sorry -- #307