have horder :=  hφ hσ 1
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
this : 1 % orderOf σ = 1
⊢ cocycle hσ hη σ = ηu hη
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
this : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ ^ 1, ⋯⟩) = 1 % orderOf σ
⊢ cocycle hσ hη σ = ηu hη