Rational spans of integer subgroups

An element of the rational span of a subgroup of integer-valued functions lies in that subgroup after multiplication by some positive integer. This denominator-clearing result is used to pass from rational spans back to integer lattices.

theorem TauCeti.AddSubgroup.exists_nat_mul_eq_intCast_of_mem_span {ι : Type u_1} {P : AddSubgroup (ι → ℤ)} {x : ι → ℚ} (hx : x ∈ Submodule.span ℚ ((fun (p : ι → ℤ) => Int.cast ∘ p) '' ↑P)) : ∃ (N : ℕ), 0 < N ∧ ∃ p ∈ P, ∀ (i : ι), ↑(p i) = ↑N * x i

An element of the rational span of a subgroup P of ι → ℤ becomes an element of P after multiplication by some positive integer.