no goals
ι : Type ?u.167752
α : Type u_1
M : Type ?u.167758
N : Type ?u.167761
P : Type ?u.167764
M₀ : Type ?u.167767
G : Type ?u.167770
R : Type ?u.167773
inst✝ : CommGroup α
a : α
l : List α
⊢ alternatingProd (a :: l) = a / alternatingProd l
rw [div_eq_mul_inv, alternatingProd_cons']