no goals
ι : Type ?u.164493
α : Type u_1
M : Type ?u.164499
N : Type ?u.164502
P : Type ?u.164505
M₀ : Type ?u.164508
G : Type ?u.164511
R : Type ?u.164514
inst✝ : CommGroup α
a : α
⊢ alternatingProd [a] = a * (alternatingProd [])⁻¹
rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
no goals
ι : Type ?u.164493
α : Type u_1
M : Type ?u.164499
N : Type ?u.164502
P : Type ?u.164505
M₀ : Type ?u.164508
G : Type ?u.164511
R : Type ?u.164514
inst✝ : CommGroup α
a b : α
l : List α
⊢ alternatingProd (a :: b :: l) = a * (alternatingProd (b :: l))⁻¹
rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]