Affine images of functions on the upper half-plane

An affine image A * f + B that is injective on the upper half-plane must have A ≠ 0.

theorem TauCeti.ne_zero_of_injOn_const_mul_add {f : ℂ → ℂ} {A B : ℂ} (h : Set.InjOn (fun (z : ℂ) => A * f z + B) UpperHalfPlane.upperHalfPlaneSet) : A ≠ 0

An affine image of a function that is injective on the upper half-plane has a nonzero linear coefficient.