Ordered integer coordinates on the range of a homomorphism

The range of a nonzero homomorphism to ℤ is order-additively isomorphic to ℤ. The inverse image of one is its positive generator. We choose the equivalence supplied by LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int.

noncomputable def AddMonoidHom.rangeOrderAddEquivInt {S : Type u_1} [AddGroup S] (c : S →+ ℤ) (hc : c ≠ 0) : ↥c.range ≃+o ℤ

Ordered integer coordinates on the range of a nonzero homomorphism to ℤ.

theorem AddMonoidHom.rangeOrderAddEquivInt_symm_one_pos {S : Type u_1} [AddGroup S] (c : S →+ ℤ) (hc : c ≠ 0) : 0 < ↑((c.rangeOrderAddEquivInt hc).symm 1)

The inverse image of one is a strictly positive integer in the range.