Theorem: associated_eta_zero_unit_spec (FltRegular/CaseII/InductionStep.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η✝ η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ≠ η₀
⊢ ↑(ε η hη) * (x + y * ↑η₀) * α η hη ^ ↑p = (x + y * ↑η) * π ^ (m * ↑p) * β η hη ^ ↑p
Tactic:
rw [mul_assoc, mul_comm (ε η hη : 𝓞 K)]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η✝ η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ≠ η₀
⊢ (x + y * ↑η₀) * α η hη ^ ↑p * ↑(ε η hη) = (x + y * ↑η) * π ^ (m * ↑p) * β η hη ^ ↑p

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η✝ η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ≠ η₀
⊢ (x + y * ↑η₀) * α η hη ^ ↑p * ↑(ε η hη) = (x + y * ↑η) * π ^ (m * ↑p) * β η hη ^ ↑p
Tactic:
exact (associated_eta_zero hp hreg hζ e hy hz η hη).choose_spec
State after:
no goals