diff --git a/FltRegular/FltRegular.lean b/FltRegular/FltRegular.lean index 6a2ff19a..7af2be36 100644 --- a/FltRegular/FltRegular.lean +++ b/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 diff --git a/FltRegular/FltThree/OddPrimeOrFour.lean b/FltRegular/FltThree/OddPrimeOrFour.lean index bb6ceac5..b99e4132 100644 --- a/FltRegular/FltThree/OddPrimeOrFour.lean +++ b/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) : diff --git a/FltRegular/NumberTheory/RegularPrimes.lean b/FltRegular/NumberTheory/RegularPrimes.lean index 9f6b1461..5d787c40 100644 --- a/FltRegular/NumberTheory/RegularPrimes.lean +++ b/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⟩ ℚ) diff --git a/blueprint/src/demo.tex b/blueprint/src/demo.tex index 60b4f2c2..999cb61c 100644 --- a/blueprint/src/demo.tex +++ b/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.