Theorem: is_cocycle (FltRegular/NumberTheory/Hilbert90.lean)

State before:
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
⊢ IsMulOneCocycle (cocycle hσ hη)
Tactic:
intro α β
State after:
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
α β : L ≃ₐ[K] L
⊢ cocycle hσ hη (α * β) = α • cocycle hσ hη β * cocycle hσ hη α

State before:
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
α β : L ≃ₐ[K] L
⊢ cocycle hσ hη (α * β) = α • cocycle hσ hη β * cocycle hσ hη α
Tactic:
simp [← Units.eq_iff, is_cocycle_aux hσ hη α β]
State after:
no goals