From c11304e880638b19f7e77b45a22771263c372acd Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Wed, 29 Nov 2023 13:11:04 +0000 Subject: [PATCH] fix --- FltRegular/NumberTheory/Hilbert92.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 68b0d37c..895885e8 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -82,4 +82,4 @@ end thm91 lemma Hilbert92 [Algebra k K] [IsGalois k K] [FiniteDimensional k K] (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) : - ∃ η : (𝓞 K)ˣ, Algebra.norm K (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := sorry + ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := sorry