diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..01f8cdb
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+.lake/
diff --git a/AlgebraInLean.lean b/AlgebraInLean.lean
new file mode 100644
index 0000000..e9ee4f3
--- /dev/null
+++ b/AlgebraInLean.lean
@@ -0,0 +1,3 @@
+-- Root module: imports all chapters of "Algebra in Lean".
+import AlgebraInLean.LittleFermat
+import AlgebraInLean.Cauchy
diff --git a/AlgebraInLean/Cauchy.lean b/AlgebraInLean/Cauchy.lean
new file mode 100644
index 0000000..a245a52
--- /dev/null
+++ b/AlgebraInLean/Cauchy.lean
@@ -0,0 +1,268 @@
+/-
+Algebra in Lean — Chapter 18
+============================
+
+This file accompanies the lecture notes "Algebra und Zahlentheorie"
+(Stefan Kebekus, CC-BY 4.0).  It translates the central key lemma
+(`lem:zsl`) and Cauchy's theorem (`Satz_von_Cauchy`) from Chapter 18
+into Lean, following the proof of the lecture notes sentence by
+sentence.  The German original of every sentence is quoted as a comment
+directly above the Lean code that implements it.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+open Equiv.Perm
+open Equiv.Perm.VectorsProdEqOne
+open MulAction
+
+/-!
+# The key lemma and Cauchy's theorem
+
+## The key lemma
+
+**Lemma (Zentrales Schlüssellemma).**  *Es sei m ∈ ℕ und es sei p eine
+Primzahl.  Weiter sei G eine Gruppe der Ordnung p^m, die auf einer
+endlichen Menge M operiert.  Weiter sei M₀ = { m ∈ M : ∀ g ∈ G: g·m = m }
+die Menge der Fixpunkte.  Dann ist |M| ≡ |M₀| (mod p).*
+
+How does Mathlib say all this?
+
+* "eine Gruppe der Ordnung p^m": Mathlib has a predicate `IsPGroup p G`
+  for this ("the order of every element is a power of p" — for finite
+  groups this is equivalent, by Cauchy's theorem below!).  The lemma
+  `IsPGroup.of_card` converts our hypothesis `Nat.card G = p ^ m` into
+  it.
+
+* "die auf einer endlichen Menge M operiert": an action of `G` on `M` is
+  a typeclass, `[MulAction G M]`; finiteness of `M` is the typeclass
+  `[Finite M]`.
+
+* The set of fixed points is `MulAction.fixedPoints G M`, and the
+  congruence `|M| ≡ |M₀| (mod p)` is written
+  `Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p]`.
+
+The proof in the lecture notes decomposes M into orbits and quotes the
+Bahnengleichung.  This is *exactly* how Mathlib proves the statement
+`IsPGroup.card_modEq_card_fixedPoints` — so here, just as the lecture
+notes quote Satz 17.2.6, we simply cite the library.
+-/
+
+theorem key_lemma {p m : ℕ} (hp : p.Prime) {G : Type*} [Group G]
+    (hG : Nat.card G = p ^ m) (M : Type*) [Finite M] [MulAction G M] :
+    Nat.card M ≡ Nat.card (fixedPoints G M) [MOD p] := by
+  have : Fact p.Prime := ⟨hp⟩
+  exact (IsPGroup.of_card hG).card_modEq_card_fixedPoints M
+
+/-!
+## Cauchy's theorem
+
+**Satz (Satz von Cauchy).**  *Wenn die Ordnung einer endlichen Gruppe
+durch p teilbar ist, dann existiert ein Element von Ordnung p.*
+
+We follow the proof of the lecture notes sentence by sentence.  The
+proof constructs a clever auxiliary set with a clever group action, so
+this time there is real work to do *before* the final theorem: we set up
+the set and the action first.
+
+„Betrachte die Menge M = { (a₁, …, a_p) ∈ G ⨯ ⋯ ⨯ G : a₁·a₂ ⋯ a_p = e }.“
+
+Mathlib knows this set.  A p-tuple of group elements is a
+`List.Vector G p` — a list of length p — and M is the set
+`Equiv.Perm.vectorsProdEqOne G p` of all vectors whose entries multiply
+to 1.
+
+„Gegeben ein Tupel (a₁, …, a_p) ∈ M, dann stellen wir erst einmal fest,
+dass der letzte Eintrag des Tupels durch die ersten Einträge eindeutig
+bestimmt ist, a_p = (a₁ ⋯ a_{p-1})⁻¹.  Wir erhalten die folgende
+Gleichung: |M| = |G^{p-1}| = |G|^{p-1}.“
+
+This, too, is already in Mathlib: the bijection
+(a₁, …, a_{p-1}) ↦ (a₁, …, a_{p-1}, (a₁ ⋯ a_{p-1})⁻¹) is
+`VectorsProdEqOne.vectorEquiv`, and the resulting counting formula is
+`VectorsProdEqOne.card`:
+-/
+
+#check @Equiv.Perm.VectorsProdEqOne.card
+-- ∀ (G : Type u_1) [inst : Group G] (n : ℕ) [inst_1 : Fintype G],
+--   Fintype.card ↥(vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)
+
+/-!
+„Als Nächstes brauchen wir eine schicke Gruppenwirkung, denn wir wollen
+das zentrale Schlüssellemma anwenden.  Dazu lassen wir die zyklische
+Gruppe ℤ/(p) auf M durch zyklisches Vertauschen wirken.“
+
+The cyclic shift of a vector `v ∈ vectorsProdEqOne G p` by k places is
+`VectorsProdEqOne.rotate v k`.  The footnote of the lecture notes — the
+shift maps M to itself „weil in jeder Gruppe aus a·b = e auch b·a = e
+gilt“ — is the Mathlib lemma `List.prod_rotate_eq_one_of_prod_eq_one`,
+which is used in the very definition of `rotate`.
+
+To let ℤ/(p) act *as a group* we must check the action axioms: rotating
+by 0 does nothing, and rotating by j + k is the same as rotating by k
+and then by j.  Mathlib provides `rotate_zero`, `rotate_rotate` and
+`rotate_length` (rotating by the full length p does nothing); from the
+last one we first derive that rotation only depends on the shift
+*modulo p* — this is why ℤ/(p), and not just ℕ, acts on M.
+-/
+
+theorem rotate_mul {G : Type*} [Group G] {p : ℕ}
+    (v : vectorsProdEqOne G p) (q : ℕ) : rotate v (p * q) = v := by
+  induction q with
+  | zero => rw [Nat.mul_zero, rotate_zero]
+  | succ q ih => rw [Nat.mul_succ, ← rotate_rotate, ih, rotate_length]
+
+theorem rotate_mod {G : Type*} [Group G] {p : ℕ}
+    (v : vectorsProdEqOne G p) (k : ℕ) : rotate v (k % p) = rotate v k := by
+  calc rotate v (k % p)
+      = rotate (rotate v (k % p)) (p * (k / p)) := (rotate_mul _ _).symm
+    _ = rotate v (k % p + p * (k / p)) := rotate_rotate _ _ _
+    _ = rotate v k := by rw [Nat.mod_add_div]
+
+/-- „Dazu lassen wir die zyklische Gruppe ℤ/(p) auf M durch zyklisches
+Vertauschen wirken.“ — An element k of ℤ/(p) acts by rotating k places.
+
+Two technical remarks.  Mathlib's `MulAction` wants a multiplicatively
+written group, while ℤ/(p) = `ZMod p` is written additively; the wrapper
+`Multiplicative` performs the change of notation.  The assumption
+`[NeZero p]` excludes p = 0, where "rotation by a residue class" would
+make no sense. -/
+instance rotateAction {G : Type*} [Group G] {p : ℕ} [NeZero p] :
+    MulAction (Multiplicative (ZMod p)) (vectorsProdEqOne G p) where
+  smul k v := rotate v (Multiplicative.toAdd k).val
+  one_smul v := by
+    show rotate v (ZMod.val 0) = v
+    rw [ZMod.val_zero, rotate_zero]
+  mul_smul j k v := by
+    show rotate v ((Multiplicative.toAdd j + Multiplicative.toAdd k).val) =
+      rotate (rotate v (Multiplicative.toAdd k).val) (Multiplicative.toAdd j).val
+    rw [ZMod.val_add, rotate_mod, rotate_rotate, Nat.add_comm]
+
+/-!
+„Die Fixpunktmenge dieser Wirkung ist M₀ = { (a, …, a) ∈ G^p : a^p = e }.“
+
+In other words: a tuple is a fixed point if and only if it is constant,
+i.e. its underlying list is `List.replicate p a` — the list (a, …, a) —
+for some a.  (The condition a^p = e then holds automatically, because
+the entries of a tuple in M multiply to e.)  The key step is the lemma
+`List.rotate_one_eq_self_iff_eq_replicate`: a list that is unchanged by
+the cyclic shift by *one* place is constant.
+-/
+
+theorem mem_fixedPoints_iff_replicate {G : Type*} [Group G] {p : ℕ}
+    [Fact (1 < p)] (v : vectorsProdEqOne G p) :
+    v ∈ fixedPoints (Multiplicative (ZMod p)) (vectorsProdEqOne G p) ↔
+      ∃ a : G, (v : List.Vector G p).toList = List.replicate p a := by
+  rw [mem_fixedPoints]
+  constructor
+  · -- A fixed point is in particular fixed by 1 ∈ ℤ/(p), so it is
+    -- unchanged by the cyclic shift by one place …
+    intro hv
+    have h1 : rotate v 1 = v := by
+      have h := hv (Multiplicative.ofAdd (1 : ZMod p))
+      rwa [show Multiplicative.ofAdd (1 : ZMod p) • v
+            = rotate v (1 : ZMod p).val from rfl, ZMod.val_one] at h
+    -- … and hence constant.
+    obtain ⟨a, ha⟩ := List.rotate_one_eq_self_iff_eq_replicate.mp
+      (Subtype.ext_iff.mp (Subtype.ext_iff.mp h1))
+    refine ⟨a, ha.trans ?_⟩
+    congr 1
+    exact (v : List.Vector G p).2
+  · -- Conversely, a constant tuple is unchanged by every cyclic shift.
+    rintro ⟨a, ha⟩ g
+    apply Subtype.ext
+    apply Subtype.ext
+    show (v : List.Vector G p).toList.rotate (Multiplicative.toAdd g).val =
+      (v : List.Vector G p).toList
+    rw [ha, List.rotate_replicate]
+
+/-!
+Now we can put the pieces together, following the lecture notes line by
+line.
+-/
+
+theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ} (hp : p.Prime)
+    (hdvd : p ∣ Fintype.card G) : ∃ a : G, orderOf a = p := by
+  -- Register the consequences of primality that instance search needs:
+  have : Fact p.Prime := ⟨hp⟩
+  have : NeZero p := ⟨hp.ne_zero⟩
+  have : Fact (1 < p) := ⟨hp.one_lt⟩
+  -- „Wir erhalten die folgende Gleichung: |M| = |G^{p-1}| = |G|^{p-1}.“
+  have hM : Nat.card (vectorsProdEqOne G p) = Fintype.card G ^ (p - 1) := by
+    rw [Nat.card_eq_fintype_card, VectorsProdEqOne.card]
+  -- „Die zyklische Gruppe ℤ/(p)“ has order p = p¹, so the key lemma
+  -- applies to the rotation action and gives |M| ≡ |M₀| (mod p):
+  have hZp : Nat.card (Multiplicative (ZMod p)) = p ^ 1 := by
+    simp [Nat.card_eq_fintype_card]
+  have hcong :
+      Nat.card (vectorsProdEqOne G p) ≡
+        Nat.card (fixedPoints (Multiplicative (ZMod p))
+          (vectorsProdEqOne G p)) [MOD p] :=
+    key_lemma hp hZp (vectorsProdEqOne G p)
+  -- „Auf der anderen Seite folgt aus dem zentralen Schlüssellemma, dass
+  --  |M₀| ≡ |M| ≡ |G|^{p-1} ≡ 0 (mod p) ist.“
+  have hdvdM0 : p ∣ Nat.card (fixedPoints (Multiplicative (ZMod p))
+      (vectorsProdEqOne G p)) := by
+    have hp1 : p - 1 ≠ 0 := by have := hp.one_lt; omega
+    have h0 : (0 : ℕ) ≡ Nat.card (fixedPoints (Multiplicative (ZMod p))
+        (vectorsProdEqOne G p)) [MOD p] :=
+      calc (0 : ℕ)
+          ≡ Fintype.card G ^ (p - 1) [MOD p] :=
+            (Nat.modEq_zero_iff_dvd.mpr (dvd_pow hdvd hp1)).symm
+        _ = Nat.card (vectorsProdEqOne G p) := hM.symm
+        _ ≡ _ [MOD p] := hcong
+    exact Nat.modEq_zero_iff_dvd.mp h0.symm
+  -- „Wegen (e, …, e) ∈ M₀ ist schon einmal klar, dass M₀ ≠ ∅ ist.“
+  let v₀ : vectorsProdEqOne G p :=
+    ⟨List.Vector.replicate p 1, (List.prod_replicate p 1).trans (one_pow p)⟩
+  have hv₀ : v₀ ∈ fixedPoints (Multiplicative (ZMod p))
+      (vectorsProdEqOne G p) :=
+    (mem_fixedPoints_iff_replicate v₀).mpr ⟨1, rfl⟩
+  -- M₀ is nonempty and its cardinality is divisible by p ≥ 2, so
+  -- |M₀| ≥ p > 1 …
+  have := Fintype.ofFinite (fixedPoints (Multiplicative (ZMod p))
+    (vectorsProdEqOne G p))
+  have hlt : 1 < Fintype.card (fixedPoints (Multiplicative (ZMod p))
+      (vectorsProdEqOne G p)) := by
+    rw [← Nat.card_eq_fintype_card]
+    have hpos : 0 < Nat.card (fixedPoints (Multiplicative (ZMod p))
+        (vectorsProdEqOne G p)) := Nat.card_pos_iff.mpr ⟨⟨⟨v₀, hv₀⟩⟩, inferInstance⟩
+    have := Nat.le_of_dvd hpos hdvdM0
+    have := hp.one_lt
+    omega
+  -- „Also existiert mindestens ein a ≠ e mit a^p = e.“
+  obtain ⟨w, hw⟩ := Fintype.exists_ne_of_one_lt_card hlt ⟨v₀, hv₀⟩
+  obtain ⟨a, ha⟩ := (mem_fixedPoints_iff_replicate w.1).mp w.2
+  -- The tuple w lies in M, so its entries multiply to e; being constant,
+  -- this says exactly a^p = e:
+  have hpow : a ^ p = 1 := by
+    have hprod : (w.1 : List.Vector G p).toList.prod = 1 := w.1.2
+    rwa [ha, List.prod_replicate] at hprod
+  -- and a ≠ e, because otherwise w would be the tuple (e, …, e) = v₀:
+  have hne : a ≠ 1 := by
+    rintro rfl
+    exact hw (Subtype.ext (Subtype.ext (Subtype.ext ha)))
+  -- „Nach Satz 17.4.11 hat a dann automatisch die Ordnung p.“
+  exact ⟨a, orderOf_eq_prime hpow hne⟩
+
+/-!
+## Remarks
+
+1. Mathlib's version of Cauchy's theorem is
+   `exists_prime_orderOf_dvd_card`; its proof is the same
+   counting argument, organized slightly differently.
+
+2. **Exercise** (Satz 18.2.3 of the lecture notes): *Es sei p eine
+   Primzahl und G eine nichttriviale Gruppe, deren Ordnung eine p-Potenz
+   ist.  Dann ist das Zentrum von G nicht trivial.*  Prove this in Lean:
+   apply `key_lemma` to the conjugation action of G on itself — or find
+   the statement in Mathlib.  Replace the `sorry` below by a proof.
+-/
+
+theorem center_nontrivial {p m : ℕ} (hp : p.Prime) {G : Type*} [Group G]
+    [Finite G] (hm : m ≠ 0) (hG : Nat.card G = p ^ m) :
+    Nontrivial (Subgroup.center G) := by
+  sorry
+
+end AlgebraInLean
diff --git a/AlgebraInLean/LittleFermat.lean b/AlgebraInLean/LittleFermat.lean
new file mode 100644
index 0000000..553cec1
--- /dev/null
+++ b/AlgebraInLean/LittleFermat.lean
@@ -0,0 +1,105 @@
+/-
+Algebra in Lean — pilot file
+============================
+
+This file accompanies the lecture notes "Algebra und Zahlentheorie"
+(Stefan Kebekus, CC-BY 4.0).  It translates one theorem of the notes —
+Fermat's little theorem, `satz:kleinerFermat` in Chapter 17 — into Lean,
+following the proof of the lecture notes *sentence by sentence*.  The
+German original of every sentence is quoted as a comment directly above
+the Lean code that implements it, so you can see how the standard
+phrases of a lecture-style proof translate into Lean/Mathlib.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+/-!
+# Fermat's little theorem
+
+**Satz (Kleiner Satz von Fermat).**  *Es sei p ∈ ℕ eine Primzahl und es
+sei a ∈ ℤ irgendeine Zahl.  Dann ist a^p ≡ a (mod p).*
+
+Before we can state this in Lean, we need to know how Mathlib speaks
+about the objects involved.
+
+* The ring ℤ/(p) of residue classes is called `ZMod p`.  The residue
+  class of an integer `a : ℤ` is written `(a : ZMod p)` — Lean inserts
+  the canonical ring morphism ℤ → ℤ/(p) automatically ("coercion").
+
+* The congruence `a ≡ b (mod p)` for integers is written
+  `a ≡ b [ZMOD p]`.
+
+* The multiplicative group 𝔽_p^* is the group of *units* of the ring
+  `ZMod p`, written `(ZMod p)ˣ`.  A unit `u : (ZMod p)ˣ` remembers its
+  inverse; the underlying ring element is again written `(u : ZMod p)`.
+
+* The lecture notes say "es sei p eine Primzahl".  In Lean we carry the
+  primality of `p` as a hypothesis `hp : p.Prime`.  Some facts —
+  for instance that ℤ/(p) is a field — are found by Lean's automation
+  only if the hypothesis is registered as an *instance*; this is what
+  the first line `have : Fact p.Prime := ⟨hp⟩` of the proof does.
+-/
+
+theorem little_fermat (p : ℕ) (hp : p.Prime) (a : ℤ) :
+    a ^ p ≡ a [ZMOD p] := by
+  have : Fact p.Prime := ⟨hp⟩
+  -- The congruence „a^p ≡ a (mod p)“ means precisely that a^p and a have
+  -- the same residue class in ℤ/(p).  So we may prove an *equation* in
+  -- the ring `ZMod p` instead; the goal becomes
+  --     (a : ZMod p) ^ p = (a : ZMod p).
+  rw [← ZMod.intCast_eq_intCast_iff]
+  push_cast
+  -- „Falls a ein Vielfaches von p ist, ist die Sache klar.“
+  by_cases ha : (a : ZMod p) = 0
+  · rw [ha, zero_pow hp.ne_zero]
+  -- „Ansonsten liefert die Restklasse von a ein nicht-verschwindendes
+  --  Element ā ∈ ℤ/(p) = 𝔽_p, also ein Element der multiplikativen
+  --  Gruppe 𝔽_p^*, …“
+  · obtain ⟨u, hu⟩ : IsUnit (a : ZMod p) := isUnit_iff_ne_zero.mpr ha
+    rw [← hu]
+    -- „… welche p−1 Elemente hat.“
+    have card_units : Nat.card (ZMod p)ˣ = p - 1 := by
+      rw [Nat.card_eq_fintype_card, ZMod.card_units p]
+    -- „Nach Satz 17.3.6 («Satz von Lagrange») ist die Ordnung von ā, also
+    --  die Größe der von ā erzeugten Untergruppe, ein Teiler von
+    --  |𝔽_p^*| = p−1.“
+    have lagrange : Nat.card (Subgroup.zpowers u) ∣ Nat.card (ZMod p)ˣ :=
+      Subgroup.card_subgroup_dvd_card (Subgroup.zpowers u)
+    have ord_dvd : orderOf u ∣ p - 1 := by
+      rw [← Nat.card_zpowers, ← card_units]
+      exact lagrange
+    -- „Es gilt also ā^(p−1) = 1 ∈ 𝔽_p^* …“
+    have pow_eq_one : u ^ (p - 1) = 1 := orderOf_dvd_iff_pow_eq_one.mp ord_dvd
+    -- „… oder äquivalent a^p ≡ a (mod p).“
+    have key : u ^ p = u := by
+      calc u ^ p = u ^ (p - 1 + 1) := by rw [Nat.sub_add_cancel hp.one_lt.le]
+        _ = u ^ (p - 1) * u := pow_succ u (p - 1)
+        _ = u := by rw [pow_eq_one, one_mul]
+    exact_mod_cast congrArg Units.val key
+
+/-!
+## Remarks
+
+1. Mathlib of course already contains Fermat's little theorem; the
+   statement about residue classes is `ZMod.pow_card`.  You can find
+   such lemmas yourself with the tactic `exact?`, or by searching on
+   https://leansearch.net or https://loogle.lean-lang.org.
+-/
+
+example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a :=
+  ZMod.pow_card a
+
+/-!
+2. **Exercise** (this is `bem:kleinerFermat` of the lecture notes).
+   In applications one often uses the equivalent formulation
+   a^(p−1) ≡ 1 (mod p) for a not divisible by p.  Derive it from
+   `little_fermat` — or give a direct proof following the ideas above.
+   Replace the `sorry` below by a proof.
+-/
+
+theorem little_fermat' (p : ℕ) (hp : p.Prime) (a : ℤ) (ha : ¬ (p : ℤ) ∣ a) :
+    a ^ (p - 1) ≡ 1 [ZMOD p] := by
+  sorry
+
+end AlgebraInLean
diff --git a/README.md b/README.md
index fe956e4..b79753b 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,40 @@
-# AlgebraInLean
+# Algebra in Lean
 
+A hands-on introduction to formalizing algebra with the proof assistant
+[Lean](https://lean-lang.org) and its mathematical library
+[Mathlib](https://leanprover-community.github.io).  The course accompanies
+the lecture notes *Algebra und Zahlentheorie* (Stefan Kebekus,
+Universität Freiburg) and is aimed at students who are learning algebra
+and have little prior experience with Lean.
+
+Selected proofs from the lecture notes are translated into Lean
+*sentence by sentence*: the German original of each sentence is quoted
+as a comment directly above the Lean code implementing it, so you can
+see how the standard phrases of a lecture-style proof translate into
+Lean/Mathlib.
+
+## Getting started
+
+1. [Install Lean](https://leanprover-community.github.io/get_started.html)
+   (`elan`, VS Code and the Lean 4 extension).
+2. Clone this repository and fetch the precompiled Mathlib cache:
+
+   ```bash
+   git clone <repository url>
+   cd AlgebraInLean
+   lake exe cache get
+   ```
+
+3. Open the folder in VS Code and start with
+   `AlgebraInLean/LittleFermat.lean`.
+
+## Contents
+
+| File | Lecture notes | Topic |
+|------|---------------|-------|
+| `AlgebraInLean/LittleFermat.lean` | Kapitel 17 | Fermat's little theorem via Lagrange |
+| `AlgebraInLean/Cauchy.lean` | Kapitel 18 | The key lemma on fixed points and Cauchy's theorem |
+
+## License
+
+CC-BY 4.0, like the lecture notes.
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..f029945
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "87adeaebd370a3b6a41ac4f044fddd4bf81803ad",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "87adeaebd370a3b6a41ac4f044fddd4bf81803ad",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0-rc2",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "AlgebraInLean",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..d272fdf
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,10 @@
+name = "AlgebraInLean"
+defaultTargets = ["AlgebraInLean"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "87adeaebd370a3b6a41ac4f044fddd4bf81803ad"
+
+[[lean_lib]]
+name = "AlgebraInLean"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..c084c7f
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.0-rc2