α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
⊢ ∀ (x : Fin (length [])), x ∈ univ → get [] x ^ (-1) ^ ↑x = 1
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
⊢ alternatingProd [] = ∏ i : Fin (length []), get [] i ^ (-1) ^ ↑i
rw [alternatingProd, Finset.prod_eq_one]
no goals
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
⊢ ∀ (x : Fin (length [])), x ∈ univ → get [] x ^ (-1) ^ ↑x = 1
rintro ⟨i, ⟨⟩⟩
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
g : G
⊢ g = ∏ i : Fin 1, get [g] i ^ (-1) ^ ↑i
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
g : G
⊢ alternatingProd [g] = ∏ i : Fin (length [g]), get [g] i ^ (-1) ^ ↑i
show g = ∏ i : Fin 1, [g].get i ^ (-1 : ℤ) ^ (i : ℕ)
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
g : G
⊢ g = get [g] 0 ^ (-1) ^ ↑0 * ∏ i : Fin 0, get [g] (Fin.succ i) ^ (-1) ^ ↑(Fin.succ i)
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
g : G
⊢ g = ∏ i : Fin 1, get [g] i ^ (-1) ^ ↑i
rw [Fin.prod_univ_succ]
no goals
α : Type ?u.237503
β : Type ?u.237506
G : Type u_1
inst✝ : CommGroup G
g : G
⊢ g = get [g] 0 ^ (-1) ^ ↑0 * ∏ i : Fin 0, get [g] (Fin.succ i) ^ (-1) ^ ↑(Fin.succ i)
simp