From 82301967aa590ff9ce91b3487be628e3d5758dfe Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@ucl.ac.uk>
Date: Mon, 4 Dec 2023 16:08:13 +0000
Subject: [PATCH] fix typo

---
 FltRegular/NumberTheory/Hilbert92.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
index fac2f81b..38fff494 100644
--- a/FltRegular/NumberTheory/Hilbert92.lean
+++ b/FltRegular/NumberTheory/Hilbert92.lean
@@ -799,8 +799,14 @@ lemma Hilbert92ish (hp : Nat.Prime p)
     obtain ⟨S, hS⟩ := Hilbert91ish p (K := K) (k := k) hp hKL σ hσ
     have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ (p : ℕ) := by
 
-      have h1 : ∀ (i : ℕ), (σ ^ i) E = ((σ ^ i)  (algebraMap k K ζ^((p : ℕ)^(h-1)))) * E :=
-        by sorry
+      have h1 : ∀ (i : ℕ), (σ ^ (i+1)) E = ((σ ^ (i+1))  (algebraMap k K ζ^((p : ℕ)^(h-1)))) * E :=
+        by
+        intro i
+        induction i
+        simp
+        sorry
+        sorry
+