Theorem: norm_eq_prod_pow_gen (FltRegular/NumberTheory/Hilbert92.lean)

State before:
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
⊢ (algebraMap k K) ((Algebra.norm k) η) = ∏ i ∈ range (orderOf σ), (σ ^ i) η
Tactic:
rw [Algebra.norm_eq_prod_automorphisms, ← Fin.prod_univ_eq_prod_range,
  ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
State after:
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 σ), (σ ^ ↑((finEquivZPowers σ ⋯).symm i)) η

State before:
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 σ), (σ ^ ↑((finEquivZPowers σ ⋯).symm i)) η
Tactic:
simp only [pow_finEquivZPowers_symm_apply]
State after:
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, σ η = ∏ x : ↑↑(Subgroup.zpowers σ), ↑x η

State before:
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, σ η = ∏ x : ↑↑(Subgroup.zpowers σ), ↑x η
Tactic:
rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i η) (Subgroup.zpowers σ)]
State after:
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 η

State before:
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 η
Tactic:
congr
State after:
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

State before:
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
Tactic:
ext
State after:
case e_s.a
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
a✝ : K ≃ₐ[k] K
⊢ a✝ ∈ univ ↔ a✝ ∈ (↑(Subgroup.zpowers σ)).toFinset

State before:
case e_s.a
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
a✝ : K ≃ₐ[k] K
⊢ a✝ ∈ univ ↔ a✝ ∈ (↑(Subgroup.zpowers σ)).toFinset
Tactic:
simp [hσ]
State after:
no goals