have := ccl.cocycle_condition 0 0 q
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c 0 q = 0
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 0 0 + c (0 + 0) q = 0 +ᵥ c 0 q + c 0 (0 + q)
⊢ c 0 q = 0