aesop (rule_sets [Metabelian, Cocycle, AutAction])
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
⊢ mul c (k, q) (inv c (k, q)) = e
no goals