Prove exists_alg_int

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

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$.