fix typo

leanprover-community · Dec 4, 2023 · 8230196 · 8230196
1 parent d6c81c5
commit 8230196
Showing 1 changed file with 8 additions and 2 deletions.
diff --git 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
+