properly fix the typo now

leanprover-community · Dec 4, 2023 · 9fe72a8 · 9fe72a8
1 parent 8230196
commit 9fe72a8
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
@@ -799,11 +799,13 @@ 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+1)) E = ((σ ^ (i+1))  (algebraMap k K ζ^((p : ℕ)^(h-1)))) * E :=
+      have h1 : ∀ (i : ℕ), (σ ^ (i+1)) E = ((σ ^ (i+1))  (algebraMap k K ζ^((p : ℕ)^(h-1)))⁻¹) * E :=
         by
         intro i
         induction i
         simp
+        rw [hE]
+
         sorry
         sorry