import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`, ermittelt mit
-- `#min_imports`.
import Mathlib.NumberTheory.LegendreSymbol.Basic
import Mathlib.Tactic.NormNum.Prime

open Verso.Genre
open Verso.Genre.Manual.InlineLean

set_option pp.rawOnError true
set_option verso.docstring.allowMissing true

#doc (Manual) "Quadratische Reziprozität" =>
%%%
htmlSplit := .never
tag := "reziprozitaet"
file := "reziprozitaet"
%%%

Das letzte Kapitel übersetzt das Rechenbeispiel zum quadratischen
Reziprozitätsgesetz aus Kapitel 24 des Skripts nach Lean — und
schließt den Kreis zum Anfang des Kurses.

# Das Mathlib-Wörterbuch

* Das Legendre-Symbol $`\left(\tfrac{a}{p}\right)` heißt
  `legendreSym p a : ℤ`; es setzt eine `Fact (Nat.Prime p)`-Instanz
  voraus.

* „$`a` ist ein quadratischer Rest modulo $`p`“ ist einfach
  `IsSquare (a : ZMod p)`.

* Das Lean-Lernthema dieses Kapitels ist die Taktik `decide`:
  Aussagen über konkrete endliche Objekte sind _entscheidbar_, etwa
  „ist 7 ein Quadrat in $`\mathbb{F}_{17}`?“.  Lean darf die Antwort
  also einfach ausrechnen.  Das Ergebnis ist ein vollwertiger
  Beweis.

# Das Reziprozitätsgesetz

Satz 24.2.1 des Skripts:

> *Satz 24.2.1 (Quadratisches Reziprozitätsgesetz).* Es seien $`p`
  und $`q` zwei unterschiedliche, ungerade Primzahlen.  Dann gilt
  die Gleichung
  $`\left(\tfrac{p}{q}\right) \cdot \left(\tfrac{q}{p}\right) = (-1)^{\frac{p-1}{2} \cdot \frac{q-1}{2}}`.

In Mathlib heißt der Satz `legendreSym.quadratic_reciprocity`.  Dort
stehen die Exponenten als `p / 2`, was für ungerade $`p` dasselbe ist
wie $`(p-1)/2`.  Dazu kommen die beiden Ergänzungssätze.  Der erste
besagt, dass $`\left(\tfrac{-1}{p}\right) = 1` genau für
$`p \equiv 1 \pmod{4}` gilt; in der Quadrat-Formulierung ist er
`ZMod.exists_sq_eq_neg_one_iff`:

```lean
example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
    IsSquare (-1 : ZMod p) :=
  ZMod.exists_sq_eq_neg_one_iff.mpr hp
```

# Das Rechenbeispiel

Aus dem Skript:

> Ist 7 ein quadratischer Rest modulo 17?
  $$`\left(\tfrac{7}{17}\right) = \left(\tfrac{17}{7}\right) \cdot (-1)^{8 \cdot 3} = \left(\tfrac{3}{7}\right) = \left(\tfrac{7}{3}\right) \cdot (-1)^{3 \cdot 1} = -\left(\tfrac{1}{3}\right) = -1.`
  Also ist die Antwort: „Nein!“

So rechnet man von Hand — und in der Klausur.  In Lean können wir
dieselbe Frage der Taktik `decide` übergeben, die das Legendre-Symbol
direkt auswertet:

```lean
instance : Fact (Nat.Prime 17) := ⟨by norm_num⟩

example : legendreSym 17 7 = -1 := by decide

example : ¬ IsSquare (7 : ZMod 17) := by decide
```

Das ist kein Widerspruch zum Skript, sondern Arbeitsteilung: Das
Reziprozitätsgesetz macht die Rechnung für _Menschen_ effizient (und
funktioniert auch bei riesigen Primzahlen); `decide` probiert stumpf
alle Restklassen durch — für kleine $`p` völlig in Ordnung.

# Rückblick

Damit endet der Kurs, wo er angefangen hat: Das Euler-Kriterium
hinter dem Legendre-Symbol beruht darauf, dass $`\mathbb{F}_p^*`
zyklisch von Ordnung $`p-1` ist — dieselbe Beobachtung, mit der wir
im Kapitel über den kleinen Satz von Fermat gerechnet haben.

# Übungsaufgabe

Ist 3 ein quadratischer Rest modulo 41?  Rechnen Sie erst von Hand
nach dem Muster des Skript-Beispiels (mit Reziprozität und den
Ergänzungssätzen).  Lassen Sie dann Lean Ihre Antwort bestätigen.
Öffnen Sie `AlgebraInLean/Reciprocity.lean` und ersetzen Sie das
`sorry` durch einen Beweis.

```lean
instance : Fact (Nat.Prime 41) := ⟨by norm_num⟩

theorem legendre_41_3 : legendreSym 41 3 = -1 := by
  sorry
```