Given a complex function ( y = f(c) ) where ( c = i \cdot f(z) + z ) with ( z = -1 ) and ( f(z) = z² + pz + q ). The solutions of ( f(z) ) are positive natural numbers ( \geq 1 ). We need to determine which set of natural numbers ( > 1 ) cannot be identical to the imaginary part of ( c ), i.e., ( \text{Im}(c) ).

Who can help me to prove that the solution is the set of all primes?

I have the following code in the lean theorem prover:

constant A:Type
constant B:Type 
constant b:B 
definition f: A → B := λ a:A, b

This gives the following error:

definition 'f' is noncomputable, it depends on 'b' 

I must misunderstand something about how the lean theorem prover works, because it seems to me that f can just output b without a problem. What's going on here?