tex update test

FltRegular/FltRegular.lean

@@ -6,11 +6,12 @@ open FltRegular
 
 /-- Statement of Fermat's last theorem for regular primes. -/
 def FltRegular.Statement : Prop :=
-  ∀ ⦃p : ℕ⦄ [Fact p.Prime], IsRegularPrime p → p ≠ 2 → FermatLastTheoremWith ℤ p
+  ∀ ⦃p : ℕ⦄ [Fact p.Prime], IsRegularPrime p → p ≠ 2 → FermatLastTheoremFor p
 
 /-- Fermat's last theorem for regular primes. -/
 theorem flt_regular {p : ℕ} [Fact p.Prime] (hreg : IsRegularPrime p) (hodd : p ≠ 2) :
-    FermatLastTheoremWith ℤ p := by
+    FermatLastTheoremFor p := by
+  apply fermatLastTheoremFor_iff_int.mpr
   intro a b c ha hb hc e
   have hprod := mul_ne_zero (mul_ne_zero ha hb) hc
   obtain ⟨e', hgcd, hprod'⟩ := MayAssume.coprime e hprod

FltRegular/FltThree/OddPrimeOrFour.lean

@@ -56,26 +56,14 @@ theorem OddPrimeOrFour.abs {z : ℤ} (h : OddPrimeOrFour z) : OddPrimeOrFour (ab
     exact ⟨hp.abs, odd_abs.mpr ho⟩
 #align odd_prime_or_four.abs OddPrimeOrFour.abs
 
-theorem OddPrimeOrFour.exists_and_dvd {n : ℤ} (n2 : 2 < n) : ∃ p, p ∣ n ∧ OddPrimeOrFour p :=
-  by
+theorem OddPrimeOrFour.exists_and_dvd {n : ℤ} (n2 : 2 < n) : ∃ p, p ∣ n ∧ OddPrimeOrFour p := by
   lift n to ℕ using (zero_lt_two.trans n2).le
-  norm_cast  at n2
-  obtain ⟨k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
-  · refine' ⟨4, ⟨2 ^ (k - 2), _⟩, Or.inl rfl⟩
+  norm_cast at n2
+  obtain h4 | ⟨p, hpprime, hpdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt n2
+  · refine ⟨4, ?_, Or.inl rfl⟩
     norm_cast
-    calc
-      2 ^ k = 2 ^ 2 * 2 ^ (k - 2) := (pow_mul_pow_sub _ ?_).symm
-      _ = 4 * 2 ^ (k - 2) := by norm_num
-
-    rcases k with (_ | _ | _)
-    · exfalso
-      norm_num at n2
-    · exfalso
-      exact lt_irrefl _ n2
-    · exact le_add_self
-  · rw [Nat.prime_iff_prime_int] at hp
-    rw [← Int.odd_coe_nat] at hodd
-    exact ⟨p, Int.coe_nat_dvd.mpr hdvd, Or.inr ⟨hp, hodd⟩⟩
+  · exact ⟨p, Int.ofNat_dvd.mpr hpdvd, Or.inr ⟨Nat.prime_iff_prime_int.mp hpprime,
+      (Int.odd_coe_nat p).mpr hpodd⟩⟩
 #align odd_prime_or_four.exists_and_dvd OddPrimeOrFour.exists_and_dvd
 
 theorem associated_of_dvd {a p : ℤ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (h : p ∣ a) :

FltRegular/NumberTheory/RegularPrimes.lean

@@ -31,7 +31,6 @@ but sadly its implementation is so unsafe that using it here creates a lot of di
 We instead put some safe specialised instances here, and we can maybe look at generalising them
 later, when this is needed. Most results from here on genuinely only work for ℚ, so this is
 very fine for the moment. -/
--- todo: now the diamond is fixed, `open_locale cyclotomic` may be fine.
 instance safe {p : ℕ+} : NumberField (CyclotomicField p ℚ) :=
   IsCyclotomicExtension.numberField {p} ℚ <| CyclotomicField p ℚ
 
@@ -49,7 +48,6 @@ variable (n p : ℕ) [Fact p.Prime]
 instance {p : ℕ} [hp : Fact p.Prime] : Fact (0 < p) :=
   ⟨hp.out.pos⟩
 
--- note that this definition can be annoying to work with whilst #14984 isn't merged.
 /-- A natural number `n` is regular if `n` is coprime with the cardinal of the class group -/
 def IsRegularNumber [hn : Fact (0 < n)] : Prop :=
   n.Coprime <| Fintype.card <| ClassGroup (𝓞 <| CyclotomicField ⟨n, hn.out⟩ ℚ)

blueprint/src/demo.tex

@@ -355,8 +355,12 @@ \section{Fermat's Last Theorem for regular primes}
 	\lean{eq_pow_prime_of_unit_of_congruent}
 	Let $p$ be a regular prime and let $u \in \ZZ[\zeta_p]^\times$. If $u \equiv a \mod p$ for some $a \in \ZZ$, then there exists $v \in \ZZ[\zeta_p]^\times$ such that $u=v^p$.
 \end{theorem}
+\begin{proof}
+\leanok
+See the Lean proof.
+\end{proof}
 
-In these next few lemmas we are following \cite{Borevich_Shafarevich}.
+In these next few lemmas we are following \cite{Borevich_Shafarevich, SD, Hilbert}.
 
 \begin{lemma}\label{lem:gen_dvd_by_frak_p}
 		Let $p$ be a regular odd prime, $x,y,z,\epsilon \in \ZZ[\zeta_p]$, $\epsilon$ a unit, and $n \in \ZZ_{\geq 1}$. Assume $x,y,z$ are coprime to $(1-\zeta_p)$ and that $x^p+y^p+\epsilon(1-\zeta_p)^{pn}z^p=0$. Then each of $(x+\zeta_p^i y)$ is divisible by $(1-\zeta_p)$ and there is a unique $i_0$ such that $(x+\zeta_p^{i_0})$ is divisible by $(1-\zeta_p)^2$.
@@ -391,6 +395,10 @@ \section{Fermat's Last Theorem for regular primes}
 	\uses{lemma:defn:is_regular_number,thm:Kummers_lemma, thm:gen_flt_eqn}
 	Let $p$ be an odd regular prime. Then \[x^p+y^p=z^p\] has no solutions with $x,y,z \in \ZZ$ and $p | xyz$.
 \end{theorem}
+\begin{proof}
+\leanok
+See the Lean proof.
+\end{proof}
 
 
 \begin{theorem}\label{FLT_regular}
@@ -399,7 +407,10 @@ \section{Fermat's Last Theorem for regular primes}
 	\uses{theorem:FLT_case_one,theorem:FLT_case_two}
 	Let $p$ be an odd regular prime.  Then \[x^p+y^p=z^p\] has no solutions with $x,y,z \in \ZZ$ and $xyz \ne 0$.
 \end{theorem}
-
+\begin{proof}
+	\leanok
+	See the Lean proof.
+\end{proof}
 \section{Kummer's Lemma}
 
 In this section we prove Theorem \ref{thm:Kummers_lemma}. The proof follows \cite{SD}. We begin with some lemmas that will be needed in the proof.
@@ -416,14 +427,15 @@ \section{Kummer's Lemma}
 \end{proof}
 
 \begin{theorem}[Hilbert 90]\label{Hilbert90}
+	\lean{Hilbert90}
 	\leanok
-	\lean{Hilbert90_integral}
 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$.
 
 \uses{lem:exists_alg_int}
 \end{theorem}
 
 \begin{proof}
+	\leanok
   Pick some $\gamma \in K$ and consider \[\beta=\gamma \a+ \sigma(\gamma)\a \sigma(\a)+\cdots+\sigma^{n-1}(\gamma)\a \sigma(\a)\cdots \sigma^{n-1}(\a),\] where $[K/F]=n$. Since the norm $\a$ is $1$ then we have $\a \sigma(\a)\cdots \sigma^{n-1}(\a)=1$ from which one verifies that $\a \sigma(\beta)=\beta$. This also uses that since we know that Galois group is cyclic, all the embeddings are given by $\sigma^i$. Note that $ \a+ \sigma\a \sigma(\a)+\cdots+\sigma^{n-1}\a \sigma(\a)\cdots \sigma^{n-1}(\a)$ is a linear combination of the embeddings $\sigma^i$. Now, using \ref{lem:lin_indep_iff_disc_ne_zero} we can check that they must be linearly independent. Therefore, it is possible to find a $\gamma$ such that $\beta \neq 0$. Putting everything together we have found $\a=\beta/\sigma(\beta)$. Using \ref{lem:exists_alg_int} we see that its possible to make sure $\beta \in \OO_K$ as required.
 
 
@@ -433,13 +445,14 @@ \section{Kummer's Lemma}
 
 
 \begin{theorem}[Hilbert 92]\label{lem:Hilbert92}
-	\leanok
 	\lean{Hilbert92}
+	\leanok
 	Let $K/F$ be a Galois extension of $F=\QQ(\zeta_p)$ with  Galois group $\Gal(K/F)$ cyclic with generator $\sigma$. Then there exists a unit $\eta \in \OO_K$ such that $N_{K/F}(\eta)=1$ but does not have the form $\epsilon/\sigma(\epsilon)$ for any unit $\e \in \OO_K$.
 
 \end{theorem}
 
 \begin{proof}
+	\leanok
 This is Hilbert theorem 92 (\cite{Hilbert}), also Lemma 33 of Swinnerton-Dyer's book (\cite{SD}).
 
 
@@ -466,14 +479,18 @@ \subsection{Some Ramification results}
 \end{lemma}
 
 \begin{proof}
+	\leanok
     This is \cite[Theorem 20]{SD}
 \end{proof}
 
 \begin{lemma}\label{lem:diff_ram}
+	\leanok
     Let $K/F$ be an extension of number fields with $\gothp_F, \gothp_K$ prime ideas in $K,F$ respectively, with $\gothp_K^e \parallel \gothp_F$ for $e >0$. Then $\gothp_K^{e-1} \mid \gothd_{K/F}$ and $\gothp_K^{e} \mid \gothd_{K/F}$ iff $\gothp_F \mid e$.
-\end{lemma}
+
+	\end{lemma}
 
 \begin{proof}
+	\leanok
     \cite[Theorem 21]{SD}
 \end{proof}
 
@@ -491,7 +508,7 @@ \subsection{Some Ramification results}
 	Let $F=\QQ(\zeta_p)$ with $\zeta_p$ a primitive $p$-th root of unity. If $\xi \in \OO_F$ and coprime to $\lam_p:=1-\zeta_p$ and if \[\xi \equiv \a_0^p \mod \lam_p^p  \] for some $\a_0 \in \OO_{F_\gothp}^\times$ (the ring of integers of the completion of $F$ at $\lam_p$), then the ideal $(\lam_p)$ is unramified in $K/F$ where $K=F(\sqrt[p]{\xi})$.
 \end{lemma}
 \begin{proof}
-    Suppose that we have $\xi = \a_0^p \mod \lam_p^{p+1}$. The using \ref{lem:loc_ramification} with $m=p-1,r=2$ gives an $\a$ such that $\a^p=\xi$ in $\OO_{F_\gothp}^\times$. Meaning that $(\lam_p)$ is split in the local extension and hence split in $K/F$ (note: add this lemma explictly somewhere).
+    Suppose that we have $\xi = \a_0^p \mod \lam_p^{p+1}$. The using \ref{lem:loc_ramification} with $m=p-1,r=2$ gives an $\a$ such that $\a^p=\xi$ in $\OO_{F_\gothp}^\times$. Meaning that $(\lam_p)$ is split in the local extension and hence split in $K/F$ (note: add this lemma explicitly somewhere).
 
     If we instead have $\lam_p^p \parallel (\xi-\a_0^p)$, then pick some element in $ K$ which agrees with $\a_0$ up to $\lam_p^{p+1}$, which we again call $\a_0$ and consider \[\eta= (\sqrt[p]{\xi}-\a_0)/\lam_p\] so that $K=F(\eta)$. Now, if $m_\eta$ is the minimal monic polynomial for $\eta$ then by definition it follows that \[m_\eta(x) \equiv x^p+\left (\a_0^{p-1}p/\lam_p^{p-1} \right )x+ (\a_0^p-\xi)/\lam_p^p \mod \lam_p\]
 
@@ -513,6 +530,7 @@ \subsection{Proof of Kummers Lemma}
 \end{lemma}
 
 \begin{proof}
+	\leanok
 	Assume $u$ is not a $p$-th power. Then let $K=F(\sqrt[p]{u})$  and $\eta \in K$ be as in \ref{lem:Hilbert92}. Then $K/F$ is Galois and cyclic of degree $p$. Now by Hilbert 90 (\ref{Hilbert90})  we can find $\beta \in \OO_K$ such that \[\eta = \beta/\sigma(\beta)\] (but note that by our assumption $\beta$ is not a unit). Note that the ideal $(\eta)$ is invariant under $\Gal(K/F)$ by construction and by \ref{lem:ramification_lem} it cannot be ramified, therefore $(\beta)$ is the extension of scalars of some ideal $\gothb$ in $\OO_F$. Now if $\gothb$ is principal generated by some $\gamma$ then $\beta=v \gamma$  for some $v \in \OO_K^\times$.
 	But this means that \[\eta = \beta/\sigma(\beta)= v/(\sigma(v)) \cdot \gamma / \sigma(\gamma)=v/\sigma(v)  \] contradicting our assumption coming from \ref{lem:Hilbert92}. On the other hand, $\gothb^p= N_{K/F}(\beta)$ is principal, meaning $p$ divides the class group of $F$ as required.