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 +