From 10f4f07fcc31be5bf7727de790e78120336dbac9 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Thu, 16 Nov 2023 12:21:59 +0100
Subject: [PATCH] Prove exists_alg_int

---
 FltRegular/NumberTheory/KummersLemma.lean | 4 ++++
 blueprint/src/demo.tex                    | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/FltRegular/NumberTheory/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma.lean
index 312dcf5e..8e0dcc9f 100644
--- a/FltRegular/NumberTheory/KummersLemma.lean
+++ b/FltRegular/NumberTheory/KummersLemma.lean
@@ -9,6 +9,10 @@ open scoped NumberField
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
 variable (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))] (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K))
 
+theorem exists_alg_int (α : K) : ∃ k : ℤ, k ≠ 0 ∧ IsAlgebraic ℤ (k • α) := by
+  obtain ⟨y, hy, h⟩ := exists_integral_multiples ℤ ℚ (L := K) {α}
+  exact ⟨y, hy, h α (Finset.mem_singleton_self _) |>.isAlgebraic⟩
+
 theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ)
     (hcong : ∃ n : ℤ, ↑p ∣ (↑u : 𝓞 K) - n) : ∃ v, u = v ^ (p : ℕ) :=
   sorry
diff --git a/blueprint/src/demo.tex b/blueprint/src/demo.tex
index dd58ebd6..7dfcdb69 100644
--- a/blueprint/src/demo.tex
+++ b/blueprint/src/demo.tex
@@ -406,8 +406,14 @@ \section{Kummer's Lemma}
 
 
 \begin{lemma}\label{lem:exists_alg_int}
+	\lean{exists_alg_int}
+	\leanok
 	Let $K$ be a number fields and $\a \in K$. Then there exists a $n \in \ZZ\backslash\{0\}$ such that $n \a$ is an algebraic integer.
 \end{lemma}
+\begin{proof}
+	\leanok
+	See mathlib.
+\end{proof}
 
 \begin{theorem}[Hilbert 90]\label{Hilbert90}
 Let $K/F$ be a Galois extension of number fields whose Galois group $\Gal(K/F)$ is cyclic with generator $\sigma$. If $\a \in K$ is such that $N_{K/F}(\a)=1$, then \[ \a =\beta/ \sigma(\beta)\] for some $\beta \in \OO_K$.