intro q
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ Function.Surjective ↑(projection c)
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ∃ a, ↑(projection c) a = q