AlgebraInLean/Book/Elements.lean

import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`, ermittelt mit
-- `#min_imports`.
import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
import Mathlib.RingTheory.Henselian
import Mathlib.RingTheory.RegularLocalRing.Defs
import Mathlib.RingTheory.SimpleRing.Principal

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

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

#doc (Manual) "Der Grad eines Elements" =>
%%%
htmlSplit := .never
tag := "elemente"
file := "elemente"
%%%

Dieses Kapitel übersetzt Satz 3.5.4 des Skripts nach Lean: Für
ein algebraisches Element $`a` stimmt der Grad $`[a:K]` des
Minimalpolynoms mit dem Grad $`[K(a):K]` der erzeugten
Körpererweiterung überein.  Zusammen mit der Gradformel aus dem
letzten Kapitel ist das das Arbeitspferd für das nächste
Kapitel, die Transitivität der Algebraizität.

# Das Mathlib-Wörterbuch

* „$`a` ist algebraisch über $`K`“ heißt `IsAlgebraic K a`.  Über
  Körpern ist das gleichbedeutend damit, dass $`a` Nullstelle
  eines _normierten_ Polynoms ist — in Mathlib `IsIntegral K a`
  („$`a` ist ganz über $`K`“).  Die Umrechnungen heißen
  `IsAlgebraic.isIntegral` und `IsIntegral.isAlgebraic`; die
  meisten Mathlib-Lemmata sind für `IsIntegral` formuliert.

* Das Minimalpolynom heißt `minpoly K a`; der Grad $`[a:K]` des
  Skripts ist sein Grad `(minpoly K a).natDegree`.  Für
  transzendentes $`a` setzt Mathlib `minpoly K a = 0`, und das
  Nullpolynom hat `natDegree` 0 — wir treffen also wieder die
  0-Konvention für $`\infty` aus dem letzten Kapitel.

* Der Zwischenkörper $`K(a)` heißt `K⟮a⟯`, kurz für
  `IntermediateField.adjoin K {a}`.  Die Klammer-Notation wird
  durch `open IntermediateField` verfügbar; Vorsicht, `⟮…⟯` sind
  eigene Unicode-Zeichen, keine gewöhnlichen Klammern.

* „Die Erweiterung $`L/K` ist algebraisch“ — jedes Element von
  $`L` ist algebraisch über $`K` — ist die Typklasse
  `Algebra.IsAlgebraic K L`.  Das elementweise Ausbuchstabieren
  übernimmt `Algebra.IsAlgebraic.isAlgebraic`.

# Satz 3.5.4

Der Satz verbindet den Grad eines Elements mit dem Grad der von
ihm erzeugten Körpererweiterung:

> *Satz 3.5.4 (Grad von Körpererweiterungen und Grad von
  Elementen).* Es sei $`L/K` eine Körpererweiterung und es sei
  $`a ∈ L`.  Dann gilt die Gleichheit $`[a:K] = [K(a):K]`.

Der Beweis im algebraischen Fall:

> _Beweis von Satz 3.5.4, falls $`a` algebraisch ist._ Setze
  $`m := [a:K]` und schreibe das Minimalpolynom von $`a` über
  $`K` als $`f(x) = λ_0 + λ_1 x + ⋯ + λ_{m-1} x^{m-1} + x^m`.
  Die Menge $`\{1, a, a^2, …, a^{m-1}\} ⊆ K(a)` ist linear
  unabhängig über $`K` …  Betrachte deshalb den
  $`m`-dimensionalen Untervektorraum
  $`V := \langle 1, a, a^2, …, a^{m-1} \rangle_K ⊆ K(a)`.
  Ich behaupte, dass $`V = K(a)` ist; damit ist dann
  $`[K(a):K] = \dim_K V = m` und der Satz ist bewiesen.  …

Die Behauptung — mit den beiden Beweisschritten
„Abgeschlossenheit unter Multiplikation“ und „Abgeschlossenheit
unter Inversenbildung“ — ist in Mathlib die Konstruktion
`IntermediateField.adjoin.powerBasis`: Für ganzes $`a` baut sie
aus den Potenzen $`1, a, …, a^{m-1}` eine Basis von `K⟮a⟯`, eine
sogenannte _Potenzbasis_.  Wie bei der Gradformel bleibt für uns
das Abzählen der Basis — und wie dort holen wir den vollständigen
Beweis am Ende des Kapitels nach.

```lean
open IntermediateField

theorem grad_element {K L : Type*} [Field K] [Field L]
    [Algebra K L] {a : L} (ha : IsIntegral K a) :
    Module.finrank K K⟮a⟯ = (minpoly K a).natDegree := by
  -- „Betrachte deshalb den m-dimensionalen Untervektorraum
  --  V := ⟨1, a, a², …, a^{m-1}⟩ ⊆ K(a).  Ich behaupte,
  --  dass V = K(a) ist …“ — die Potenzbasis von K⟮a⟯:
  let pb := IntermediateField.adjoin.powerBasis ha
  -- „… damit ist dann [K(a):K] = dim_K V = m und der Satz
  --  ist bewiesen.“
  rw [Module.finrank_eq_card_basis pb.basis,
    Fintype.card_fin]
  rfl
```

Den transzendenten Fall — $`[a:K] = ∞ = [K(a):K]` — behandelt
das Skript mit den unendlichen Potenzen $`1, a, a^2, …`; in
Mathlibs 0-Konvention steht auf beiden Seiten schlicht 0.  Als
fertiges Zitat heißt unser Satz übrigens
`IntermediateField.adjoin.finrank`.

# Übungsaufgabe

Das erste Korollar des Skripts zu Satz 3.5.4:

> Es sei $`L/K` eine Körpererweiterung und es sei $`a ∈ L`.
  Falls $`[a:K] < ∞` ist, dann ist $`K(a)` algebraisch
  über $`K`.

Die beiden Zutaten kennt Mathlib als
`IntermediateField.adjoin.finiteDimensional` („der Grad ist
endlich“) und `Algebra.IsAlgebraic.of_finite` („endliche
Erweiterungen sind algebraisch“).  Beachten Sie, dass die
Endlichkeit mit `have := …` in den Kontext geholt werden muss,
damit die Instanzsuche sie sieht.  Öffnen Sie
`AlgebraInLean/Elements.lean` und ersetzen Sie das `sorry`
durch einen Beweis.

```lean
theorem einfach_algebraisch {K L : Type*} [Field K]
    [Field L] [Algebra K L] {a : L}
    (ha : IsIntegral K a) :
    Algebra.IsAlgebraic K K⟮a⟯ := by
  sorry
```

# Der vollständige Beweis

Oben haben wir die eigentliche Arbeit — die Potenzen bilden eine
Basis von $`K(a)` — bei `IntermediateField.adjoin.powerBasis`
eingekauft.  Jetzt führen wir den Skript-Beweis Satz für Satz
selbst aus.  Er ist deutlich länger als der vollständige Beweis
der Gradformel, denn das Skript zeigt hier wirklich etwas
Substantielles: dass ein endlichdimensionaler Untervektorraum,
der unter Multiplikation abgeschlossen ist, automatisch auch
Inverse enthält.

Die Hauptfigur ist der Untervektorraum aus dem Skript:

> Betrachte deshalb den $`m`-dimensionalen Untervektorraum
  $`V := \langle 1, a, a^2, …, a^{m-1} \rangle_K ⊆ K(a)`.

```lean
open Polynomial

variable {K L : Type*} [Field K] [Field L] [Algebra K L]

-- Der Untervektorraum V = ⟨1, a, …, a^{m-1}⟩ des Skripts.
noncomputable def potenzraum (K : Type*) {L : Type*}
    [Field K] [Field L] [Algebra K L] (a : L) :
    Submodule K L :=
  Submodule.span K (Set.range
    fun i : Fin (minpoly K a).natDegree => a ^ (i : ℕ))
```

Ein Argument benutzt das Skript zweimal — einmal für $`a`, später
noch einmal für ein Element $`y ∈ V`:

> Falls nicht, dann gäbe es eine Zahl $`m ∈ ℕ` und Elemente
  $`λ_0, …, λ_m ∈ K`, die nicht alle gleich Null sind, sodass
  $`0 = \sum_{i} λ_i \cdot a^i` ist.  Dann wäre $`a` aber eine
  Nullstelle des Polynoms $`f(x) = \sum_i λ_i \cdot x^i ∈ K[x]`,
  welches nicht das Nullpolynom ist.

Wir formulieren es deshalb als eigenes Hilfslemma: Eine
nichttriviale lineare Relation unter den Potenzen liefert ein
Polynom.

```lean
theorem polynom_aus_relation {k : ℕ} (y : L) (μ : Fin k → K)
    (hrel : ∑ i, μ i • y ^ (i : ℕ) = 0) (i₀ : Fin k)
    (hμ : μ i₀ ≠ 0) :
    ∃ g : K[X],
      g ≠ 0 ∧ g.degree < (k : ℕ) ∧ aeval y g = 0 := by
  -- Das Polynom g = ∑ μᵢ·xⁱ …
  refine ⟨∑ i : Fin k, C (μ i) * X ^ (i : ℕ), ?_, ?_, ?_⟩
  -- „… welches nicht das Nullpolynom ist“: sein i₀-ter
  -- Koeffizient ist μᵢ₀ ≠ 0.
  · intro h0
    apply hμ
    have hc := congrArg (fun g => coeff g (i₀ : ℕ)) h0
    simpa [finsetSum_coeff, coeff_C_mul, coeff_X_pow,
      Fin.val_inj] using hc
  -- … hat Grad < k …
  · refine lt_of_le_of_lt (degree_sum_le _ _) ?_
    rw [Finset.sup_lt_iff
      (by exact_mod_cast WithBot.bot_lt_coe k)]
    intro i _
    exact lt_of_le_of_lt (degree_C_mul_X_pow_le _ _)
      (by exact_mod_cast i.isLt)
  -- … und „y wäre eine Nullstelle des Polynoms“.
  · rw [map_sum]
    simp_rw [map_mul, aeval_C, map_pow, aeval_X,
      ← Algebra.smul_def]
    exact hrel
```

Damit folgt die lineare Unabhängigkeit wie im Skript:

> Die Menge $`\{1, a, a^2, …, a^{m-1}\} ⊆ K(a)` ist linear
  unabhängig über $`K`: Jede nicht-triviale Linearkombination
  der Null lieferte nämlich ein Polynom vom Grad kleiner $`m`,
  welches nicht das Nullpolynom ist und $`a` als Nullstelle
  hat — im Widerspruch zur Minimalität des Grades des
  Minimalpolynoms.

Die „Minimalität des Grades“ heißt in Mathlib
`minpoly.degree_le_of_ne_zero`.

```lean
theorem potenzen_unabhaengig {a : L} (ha : IsIntegral K a) :
    LinearIndependent K
      (fun i : Fin (minpoly K a).natDegree =>
        a ^ (i : ℕ)) := by
  rw [Fintype.linearIndependent_iff]
  intro μ hrel i₀
  by_contra hμ
  -- „Jede nicht-triviale Linearkombination der Null
  --  lieferte ein Polynom vom Grad kleiner m … mit a als
  --  Nullstelle“
  obtain ⟨g, hg0, hdeg, hroot⟩ :=
    polynom_aus_relation a μ hrel i₀ hμ
  -- „im Widerspruch zur Minimalität des Grades des
  --  Minimalpolynoms.“
  have hle := minpoly.degree_le_of_ne_zero K a hg0 hroot
  rw [degree_eq_natDegree (minpoly.ne_zero ha)] at hle
  exact absurd (hle.trans_lt hdeg) (lt_irrefl _)
```

Nun der erste Schritt des Skripts:

> _Schritt 1: Abgeschlossenheit unter Multiplikation._ Weil
  $`a` eine Nullstelle des Minimalpolynoms $`f` ist, gilt die
  Gleichung $`a^m = -\sum_{i=0}^{m-1} λ_i \cdot a^i ∈ V`.
  Durch wiederholte Anwendung dieser Gleichung folgt induktiv,
  dass $`a^n ∈ V` ist, für alle Zahlen $`n ∈ ℕ`.  Jedes Produkt
  von Elementen aus $`V` ist eine $`K`-Linearkombination von
  Potenzen von $`a`, also gilt für alle $`v_1, v_2 ∈ V`, dass
  $`v_1 \cdot v_2 ∈ V` ist.

```lean
-- „Weil a eine Nullstelle des Minimalpolynoms f ist, gilt
--  die Gleichung a^m = -∑ λᵢ·aⁱ.“
theorem hoechste_potenz {a : L} (ha : IsIntegral K a) :
    a ^ (minpoly K a).natDegree =
      -∑ i ∈ Finset.range (minpoly K a).natDegree,
        (minpoly K a).coeff i • a ^ i := by
  have h := minpoly.aeval K a
  rw [aeval_eq_sum_range, Finset.sum_range_succ,
    (minpoly.monic ha).coeff_natDegree, one_smul] at h
  exact eq_neg_of_add_eq_zero_right h

-- „Durch wiederholte Anwendung dieser Gleichung folgt
--  induktiv, dass aⁿ ∈ V ist, für alle Zahlen n ∈ ℕ.“
theorem potenz_mem {a : L} (ha : IsIntegral K a) (n : ℕ) :
    a ^ n ∈ potenzraum K a := by
  induction n using Nat.strong_induction_on with
  | _ n IH =>
    by_cases hn : n < (minpoly K a).natDegree
    · exact Submodule.subset_span ⟨⟨n, hn⟩, rfl⟩
    · rw [not_lt] at hn
      have hm0 : 0 < (minpoly K a).natDegree :=
        minpoly.natDegree_pos ha
      have hsplit : a ^ n =
          a ^ (n - (minpoly K a).natDegree)
            * a ^ (minpoly K a).natDegree := by
        rw [← pow_add]
        congr 1
        omega
      rw [hsplit, hoechste_potenz ha, mul_neg,
        Finset.mul_sum]
      refine Submodule.neg_mem _
        (Submodule.sum_mem _ fun i hi => ?_)
      rw [mul_smul_comm, ← pow_add]
      refine Submodule.smul_mem _ _ (IH _ ?_)
      have := Finset.mem_range.mp hi
      omega

-- „Jedes Produkt von Elementen aus V ist eine
--  K-Linearkombination von Potenzen von a, also gilt für
--  alle v₁, v₂ ∈ V, dass v₁·v₂ ∈ V ist.“
theorem produkt_mem {a : L} (ha : IsIntegral K a) {x y : L}
    (hx : x ∈ potenzraum K a) (hy : y ∈ potenzraum K a) :
    x * y ∈ potenzraum K a := by
  induction hx, hy using Submodule.span_induction₂ with
  | mem_mem u v hu hv =>
    obtain ⟨i, rfl⟩ := hu
    obtain ⟨j, rfl⟩ := hv
    simpa [pow_add] using potenz_mem ha ((i : ℕ) + (j : ℕ))
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u v w _ _ hw h1 h2 =>
    rw [add_mul]
    exact Submodule.add_mem _ h1 h2
  | add_right u v w hu _ _ h1 h2 =>
    rw [mul_add]
    exact Submodule.add_mem _ h1 h2
  | smul_left r u v _ _ h =>
    rw [smul_mul_assoc]
    exact Submodule.smul_mem _ _ h
  | smul_right r u v _ _ h =>
    rw [mul_smul_comm]
    exact Submodule.smul_mem _ _ h
```

Das „Jedes Produkt … ist eine $`K`-Linearkombination“ erledigt
`Submodule.span_induction₂`: Es genügt, die Behauptung für die
erzeugenden Potenzen zu prüfen (der Fall `mem_mem`, dort ist
$`a^i \cdot a^j = a^{i+j}`); Summen und Vielfache vererben sich.

Der zweite Schritt ist das Herzstück:

> _Schritt 2: Abgeschlossenheit unter Inversenbildung._ Es sei
  $`y ∈ V` mit $`y ≠ 0` gegeben.  Weil $`V` abgeschlossen unter
  der Multiplikation ist, liegen alle Potenzen
  $`1, y, y^2, …, y^m` in $`V`.  Das sind $`m+1` Elemente in
  einem Vektorraum der Dimension $`m`, also sind diese Elemente
  linear abhängig über $`K`.  Insbesondere ist $`y` algebraisch
  über $`K`.  Es sei $`g(x) = c_0 + c_1 x + ⋯ + x^n` das
  Minimalpolynom von $`y` über $`K`.  Dann ist $`c_0 ≠ 0`:
  Andernfalls könnte ich nämlich in $`g` einmal $`x`
  ausklammern, also $`g = x \cdot h` schreiben.  Weil $`K(a)`
  ein Körper und $`y ≠ 0` ist, folgte aus
  $`0 = g(y) = y \cdot h(y)` schon $`h(y) = 0` — im Widerspruch
  zur Minimalität des Grades von $`g`.  Aus der Gleichung
  $`0 = g(y) = y \cdot (y^{n-1} + c_{n-1} y^{n-2} + ⋯ + c_1) + c_0`
  folgt jetzt $`1/y = (y^{n-1} + ⋯ + c_1)/(-c_0) ∈ V`, denn der
  Zähler ist eine $`K`-Linearkombination von Potenzen von $`y`,
  liegt also in $`V`, und der Nenner $`-c_0` liegt in $`K`.

Das Zählargument „$`m+1` Elemente in Dimension $`m`“ ist
`LinearIndependent.fintype_card_le_finrank`; die Dimension von
$`V` kennen wir aus der linearen Unabhängigkeit
(`finrank_span_eq_card`).

```lean
theorem invers_mem {a : L} (ha : IsIntegral K a) {y : L}
    (hy : y ∈ potenzraum K a) (hy0 : y ≠ 0) :
    y⁻¹ ∈ potenzraum K a := by
  -- „Weil V abgeschlossen unter der Multiplikation ist,
  --  liegen alle Potenzen 1, y, y², … in V.“
  have hyn : ∀ j : ℕ, y ^ j ∈ potenzraum K a := by
    intro j
    induction j with
    | zero => simpa using potenz_mem ha 0
    | succ j IH =>
      rw [pow_succ]
      exact produkt_mem ha IH hy
  -- „Das sind m+1 Elemente in einem Vektorraum der
  --  Dimension m, also sind diese Elemente linear abhängig
  --  über K.“
  have hfin : FiniteDimensional K (potenzraum K a) := by
    unfold potenzraum
    exact FiniteDimensional.span_of_finite K
      (Set.finite_range _)
  have hdim : Module.finrank K (potenzraum K a)
      = (minpoly K a).natDegree := by
    unfold potenzraum
    rw [finrank_span_eq_card (potenzen_unabhaengig ha),
      Fintype.card_fin]
  have habh : ¬ LinearIndependent K
      (fun i : Fin ((minpoly K a).natDegree + 1) =>
        (⟨y ^ (i : ℕ), hyn i⟩ : potenzraum K a)) := by
    intro h
    have hcard := h.fintype_card_le_finrank
    rw [Fintype.card_fin, hdim] at hcard
    omega
  -- „Insbesondere ist y algebraisch über K.“
  rw [Fintype.not_linearIndependent_iff] at habh
  obtain ⟨μ, hrel, i₀, hμ0⟩ := habh
  have hrelL : ∑ i : Fin ((minpoly K a).natDegree + 1),
      μ i • y ^ (i : ℕ) = 0 := by
    simpa using congrArg
      (Submodule.subtype (potenzraum K a)) hrel
  obtain ⟨g, hg0, _, hgroot⟩ :=
    polynom_aus_relation y μ hrelL i₀ hμ0
  have hyint : IsIntegral K y :=
    (IsAlgebraic.isIntegral ⟨g, hg0, hgroot⟩)
  -- „Es sei g das Minimalpolynom von y über K.  Dann ist
  --  c₀ ≠ 0: Andernfalls könnte ich nämlich in g einmal x
  --  ausklammern, also g = x·h schreiben.  Weil K(a) ein
  --  Körper und y ≠ 0 ist, folgte aus 0 = g(y) = y·h(y)
  --  schon h(y) = 0 — im Widerspruch zur Minimalität des
  --  Grades von g.“
  have hc0 : (minpoly K y).coeff 0 ≠ 0 := by
    intro h0
    obtain ⟨h, hh⟩ := X_dvd_iff.mpr h0
    have hhy : aeval y h = 0 := by
      have haev := minpoly.aeval K y
      rw [hh, map_mul, aeval_X] at haev
      rcases mul_eq_zero.mp haev with h1 | h1
      · exact absurd h1 hy0
      · exact h1
    have hhne : h ≠ 0 := by
      rintro rfl
      rw [mul_zero] at hh
      exact minpoly.ne_zero hyint hh
    have hle := minpoly.degree_le_of_ne_zero K y hhne hhy
    rw [hh, mul_comm] at hle
    exact absurd hle
      (not_le.mpr (degree_lt_degree_mul_X hhne))
  -- „Aus der Gleichung 0 = g(y) = y·(y^{n-1} + ⋯ + c₁) + c₀
  --  folgt jetzt 1/y = (y^{n-1} + ⋯ + c₁)/(-c₀) ∈ V …“
  have expand := minpoly.aeval K y
  rw [aeval_eq_sum_range, Finset.sum_range_succ'] at expand
  simp_rw [pow_succ, ← smul_mul_assoc, pow_zero] at expand
  rw [← Finset.sum_mul] at expand
  have hwy : (∑ i ∈ Finset.range (minpoly K y).natDegree,
        (minpoly K y).coeff (i + 1) • y ^ i) * y
      = -((minpoly K y).coeff 0 • 1) :=
    eq_neg_of_add_eq_zero_left expand
  have hone : y * ((-(minpoly K y).coeff 0)⁻¹ •
      ∑ i ∈ Finset.range (minpoly K y).natDegree,
        (minpoly K y).coeff (i + 1) • y ^ i) = 1 := by
    rw [mul_smul_comm, mul_comm y, hwy, ← neg_smul,
      smul_smul, inv_mul_cancel₀ (neg_ne_zero.mpr hc0),
      one_smul]
  rw [inv_eq_of_mul_eq_one_right hone]
  -- „… denn der Zähler ist eine K-Linearkombination von
  --  Potenzen von y, liegt also in V, und der Nenner -c₀
  --  liegt in K.“
  exact Submodule.smul_mem _ _
    (Submodule.sum_mem _ fun i _ =>
      Submodule.smul_mem _ _ (hyn i))
```

Bleibt der Zusammenbau:

> Ich behaupte, dass $`V = K(a)` ist; damit ist dann
  $`[K(a):K] = \dim_K V = m` und der Satz ist bewiesen.  Um die
  Behauptung zu zeigen, genügt es zu zeigen, dass $`V` ein
  Unterkörper von $`K(a)` ist.  Denn $`V` enthält $`K` und das
  Element $`a`, und $`K(a)` ist per Definition der kleinste
  Unterkörper, der $`K` und $`a` enthält.  Weil $`V` ein
  Untervektorraum ist, ist $`V` abgeschlossen unter der
  Addition.

Das „Bündeln“ von $`V` mit den bewiesenen Abgeschlossenheiten zu
einem Unterkörper ist in Lean das Ausfüllen der Strukturfelder
von `Subalgebra` und `IntermediateField`; das „per Definition
der kleinste Unterkörper“ ist `adjoin_simple_le_iff`.

```lean
theorem grad_element_vollstaendig {a : L}
    (ha : IsIntegral K a) :
    Module.finrank K K⟮a⟯ = (minpoly K a).natDegree := by
  -- „… genügt es zu zeigen, dass V ein Unterkörper von K(a)
  --  ist.“ — wir bündeln V zu einem Zwischenkörper F:
  let A : Subalgebra K L :=
    { carrier := potenzraum K a
      mul_mem' := fun hx hy => produkt_mem ha hx hy
      one_mem' := by simpa using potenz_mem ha 0
      add_mem' := fun hx hy => Submodule.add_mem _ hx hy
      zero_mem' := Submodule.zero_mem _
      algebraMap_mem' := fun c => by
        rw [Algebra.algebraMap_eq_smul_one]
        exact Submodule.smul_mem _ _
          (by simpa using potenz_mem ha 0) }
  let F : IntermediateField K L :=
    { A with
      inv_mem' := fun x hx => by
        by_cases hx0 : x = 0
        · rw [hx0, inv_zero]
          exact Submodule.zero_mem _
        · exact invers_mem ha hx hx0 }
  -- „Denn V enthält K und das Element a, und K(a) ist per
  --  Definition der kleinste Unterkörper, der K und a
  --  enthält.“
  have haF : a ∈ F := by
    show a ∈ potenzraum K a
    simpa using potenz_mem ha 1
  have oben : K⟮a⟯ ≤ F := adjoin_simple_le_iff.mpr haF
  have unten : F ≤ K⟮a⟯ := by
    intro x hx
    have hVsub : potenzraum K a ≤
        Subalgebra.toSubmodule K⟮a⟯.toSubalgebra := by
      unfold potenzraum
      rw [Submodule.span_le]
      rintro _ ⟨i, rfl⟩
      exact pow_mem (mem_adjoin_simple_self K a) _
    exact hVsub hx
  have hFK : F = K⟮a⟯ := le_antisymm unten oben
  -- „… damit ist dann [K(a):K] = dim_K V = m und der Satz
  --  ist bewiesen.“
  rw [← hFK]
  have h1 : Module.finrank K F
      = Module.finrank K (potenzraum K a) :=
    (Subalgebra.finrank_toSubmodule A).symm
  rw [h1]
  unfold potenzraum
  rw [finrank_span_eq_card (potenzen_unabhaengig ha),
    Fintype.card_fin]
```