simp_all only [add_right_neg, left_id, add_zero, AutAction.vadd_eq, add_left_neg, right_id]
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)
⊢ c q (-q) = q +ᵥ c (-q) q
no goals