no goals
ι : Type ?u.19288
α : Type u_1
M : Type ?u.19294
N : Type ?u.19297
P : Type ?u.19300
M₀ : Type ?u.19303
G : Type ?u.19306
R : Type ?u.19309
inst✝ : CommGroup α
⊢ alternatingProd (reverse []) = alternatingProd [] ^ (-1) ^ (length [] + 1)
simp only [alternatingProd_nil, one_zpow, reverse_nil]
ι : Type ?u.19288
α : Type u_1
M : Type ?u.19294
N : Type ?u.19297
P : Type ?u.19300
M₀ : Type ?u.19303
G : Type ?u.19306
R : Type ?u.19309
inst✝ : CommGroup α
a : α
l : List α
⊢ (alternatingProd l ^ (-1) ^ length l)⁻¹ * a ^ (-1) ^ length l = (a / alternatingProd l) ^ (-1) ^ length l
ι : Type ?u.19288
α : Type u_1
M : Type ?u.19294
N : Type ?u.19297
P : Type ?u.19300
M₀ : Type ?u.19303
G : Type ?u.19306
R : Type ?u.19309
inst✝ : CommGroup α
a : α
l : List α
⊢ alternatingProd (reverse (a :: l)) = alternatingProd (a :: l) ^ (-1) ^ (length (a :: l) + 1)
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
  alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ, neg_mul,
  one_mul, zpow_neg, inv_inv]
no goals
ι : Type ?u.19288
α : Type u_1
M : Type ?u.19294
N : Type ?u.19297
P : Type ?u.19300
M₀ : Type ?u.19303
G : Type ?u.19306
R : Type ?u.19309
inst✝ : CommGroup α
a : α
l : List α
⊢ (alternatingProd l ^ (-1) ^ length l)⁻¹ * a ^ (-1) ^ length l = (a / alternatingProd l) ^ (-1) ^ length l
rw [mul_comm, ← div_eq_mul_inv, div_zpow]