add some comments (for example mathlib PR numbers)

ImperialCollegeLondon · Jan 7, 2025 · 35bb6ec · 35bb6ec
1 parent e66b7d1
commit 35bb6ec
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 1 deletion.
diff --git a/FLT/Mathlib/NumberTheory/NumberField/Basic.lean b/FLT/Mathlib/NumberTheory/NumberField/Basic.lean
@@ -2,6 +2,7 @@ import Mathlib.NumberTheory.NumberField.Basic
 
 open scoped NumberField
 
+-- Mathlib PR #20544
 theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) :
     (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
   obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z

diff --git a/FLT/NumberField/InfiniteAdeleRing.lean b/FLT/NumberField/InfiniteAdeleRing.lean
@@ -6,13 +6,15 @@ open NumberField
 
 variable [Algebra K (InfiniteAdeleRing L)] [IsScalarTower K L (InfiniteAdeleRing L)]
 
+-- TODO should be →A[K]
 /-- The canonical map from the infinite adeles of K to the infinite adeles of L -/
 def NumberField.InfiniteAdeleRing.baseChange :
     InfiniteAdeleRing K →ₐ[K] InfiniteAdeleRing L :=
   sorry
 
 open scoped TensorProduct
 
+-- TODO should be ≃A[L]
 /-- The canonical `L`-algebra isomorphism from `L ⊗_K K_∞` to `L_∞` induced by the
 `K`-algebra base change map `K_∞ → L_∞`. -/
 def NumberField.InfiniteAdeleRing.baseChangeIso :

diff --git a/FLT/NumberField/IsTotallyReal.lean b/FLT/NumberField/IsTotallyReal.lean
@@ -1,5 +1,11 @@
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.Data.Complex.Basic
 
-class NumberField.IsTotallyReal (F : Type*) [Field F] [NumberField F] : Prop where
+namespace NumberField
+
+-- #20542
+class IsTotallyReal (F : Type*) [Field F] [NumberField F] : Prop where
   isTotallyReal : ∀ τ : F →+* ℂ, ∀ f : F, ∃ r : ℝ, τ f = r
+
+instance : IsTotallyReal ℚ where
+  isTotallyReal τ q := ⟨q, by simp⟩