Theorem: Hilbert90 (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
⊢ ∃ ε, η = ε / σ ε
Tactic:
by_cases hone : orderOf σ = 1
State after:
case pos
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
⊢ ∃ ε, η = ε / σ ε

case neg
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
⊢ ∃ ε, η = ε / σ ε

State before:
case neg
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
⊢ ∃ ε, η = ε / σ ε
Tactic:
obtain ⟨ε, hε⟩ := isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units _ (is_cocycle hσ hη)
State after:
case neg.intro
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
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ ∃ ε, η = ε / σ ε

State before:
case neg.intro
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
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ ∃ ε, η = ε / σ ε
Tactic:
use ε⁻¹
State after:
case 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
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ / σ (↑ε)⁻¹

State before:
case 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
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ / σ (↑ε)⁻¹
Tactic:
simp only [map_inv₀, div_inv_eq_mul]
State after:
case 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
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ * σ ↑ε

State before:
case 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
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
specialize hε σ
State after:
case 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
ε : Lˣ
hε : σ • ε / ε = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε

State before:
case 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
ε : Lˣ
hε : σ • ε / ε = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
nth_rewrite 2 [← inv_inv ε] at hε
State after:
case 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
ε : Lˣ
hε : σ • ε / ε⁻¹⁻¹ = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε

State before:
case 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
ε : Lˣ
hε : σ • ε / ε⁻¹⁻¹ = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
rw [div_inv_eq_mul, cocycle_spec hσ hη hone, mul_inv_eq_iff_eq_mul, mul_comm, ← Units.eq_iff] at hε
State after:
case 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
ε : Lˣ
hε : ↑(σ • ε) = ↑(ε * ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε

State before:
case 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
ε : Lˣ
hε : ↑(σ • ε) = ↑(ε * ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
simp only [AlgEquiv.smul_units_def, Units.coe_map, MonoidHom.coe_coe, Units.val_mul] at hε
State after:
case 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
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε

State before:
case 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
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
symm
State after:
case 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
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ (↑ε)⁻¹ * σ ↑ε = η

State before:
case 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
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ (↑ε)⁻¹ * σ ↑ε = η
Tactic:
rw [inv_mul_eq_iff_eq_mul₀ ε.ne_zero, hε]
State after:
case 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
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ ↑ε * ↑(ηu hη) = ↑ε * η

State before:
case 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
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ ↑ε * ↑(ηu hη) = ↑ε * η
Tactic:
rfl
State after:
no goals

State before:
case pos
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
⊢ ∃ ε, η = ε / σ ε
Tactic:
suffices finrank K L = 1 by
  obtain ⟨a, ha⟩ := mem_span_singleton.1 <| (eq_top_iff'.1 <|
    (finrank_eq_one_iff_of_nonzero _ one_ne_zero).1 this) η
  rw [← Algebra.algebraMap_eq_smul_one] at ha
  rw [← ha, Algebra.norm_algebraMap, this, pow_one] at hη
  exact ⟨1, by simp [← ha, hη]⟩
State after:
case pos
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
⊢ finrank K L = 1

State before:
case pos
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
⊢ finrank K L = 1
Tactic:
rw [← IsGalois.card_aut_eq_finrank, Fintype.card_eq_one_iff]
State after:
case pos
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
⊢ ∃ x, ∀ (y : L ≃ₐ[K] L), y = x

State before:
case pos
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
⊢ ∃ x, ∀ (y : L ≃ₐ[K] L), y = x
Tactic:
refine ⟨σ, fun τ ↦ ?_⟩
State after:
case pos
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
τ : L ≃ₐ[K] L
⊢ τ = σ

State before:
case pos
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
τ : L ≃ₐ[K] L
⊢ τ = σ
Tactic:
simp only [orderOf_eq_one_iff.1 hone, Subgroup.zpowers_one_eq_bot, Subgroup.mem_bot] at hσ
State after:
case pos
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
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
τ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x = 1
⊢ τ = σ

State before:
case pos
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
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
τ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x = 1
⊢ τ = σ
Tactic:
rw [orderOf_eq_one_iff.1 hone, hσ τ]
State after:
no goals

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
hone : orderOf σ = 1
this : finrank K L = 1
⊢ ∃ ε, η = ε / σ ε
Tactic:
obtain ⟨a, ha⟩ := mem_span_singleton.1 <| (eq_top_iff'.1 <|
  (finrank_eq_one_iff_of_nonzero _ one_ne_zero).1 this) η
State after:
case intro
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
this : finrank K L = 1
a : K
ha : a • 1 = η
⊢ ∃ ε, η = ε / σ ε

State before:
case intro
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
this : finrank K L = 1
a : K
ha : a • 1 = η
⊢ ∃ ε, η = ε / σ ε
Tactic:
rw [← Algebra.algebraMap_eq_smul_one] at ha
State after:
case intro
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
this : finrank K L = 1
a : K
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε

State before:
case intro
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
this : finrank K L = 1
a : K
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε
Tactic:
rw [← ha, Algebra.norm_algebraMap, this, pow_one] at hη
State after:
case intro
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
hone : orderOf σ = 1
this : finrank K L = 1
a : K
hη : a = 1
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε

State before:
case intro
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
hone : orderOf σ = 1
this : finrank K L = 1
a : K
hη : a = 1
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε
Tactic:
exact ⟨1, by simp [← ha, hη]⟩
State after:
no goals

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
hone : orderOf σ = 1
this : finrank K L = 1
a : K
hη : a = 1
ha : (algebraMap K L) a = η
⊢ η = 1 / σ 1
Tactic:
simp [← ha, hη]
State after:
no goals