how to claim the image of a homomorphism

Stream: new members

[Chengyan Hu]

Hi! I want to state a galois representation with image {-1,1} in lean, I know I should write it as a morphism form GQp to multiplicative group of Z, but I'm still confused about how to write down the image is {-1,1}.
image.png

[Aaron Liu]

write it as a monoid hom into ℤˣ

[Chengyan Hu]

yep I already know that, but how should I claim the image is exactly {-1,1}?

[Aaron Liu]

prove it's surjective

[Aaron Liu]

docs#Function.Surjective