congr
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝¹ : H
hσ✝¹ : Subgroup.zpowers σ✝¹ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ✝ : K ≃ₐ[k] K
hσ✝ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ✝
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
η : K
⊢ ∏ σ : K ≃ₐ[k] K, σ η = ∏ i ∈ (↑(Subgroup.zpowers σ)).toFinset, i η
case e_s
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝¹ : H
hσ✝¹ : Subgroup.zpowers σ✝¹ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ✝ : K ≃ₐ[k] K
hσ✝ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ✝
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
η : K
⊢ univ = (↑(Subgroup.zpowers σ)).toFinset