Arithmetic of torsion-free lattices

This module isolates numerical lattice facts that require only a torsion-free ℤ-module and no geometric realization.

NoZeroSMulDivisors ℤ Λ is exactly torsion-freeness for an additive group: n • x = 0 → n = 0 ∨ x = 0.

theorem IntegralLattice.eq_zero_of_zsmul_eq_zero {Λ : Type u_1} [AddCommGroup Λ] [NoZeroSMulDivisors ℤ Λ] {n : ℤ} (hn : n ≠ 0) {x : Λ} (h : n • x = 0) : x = 0

In a torsion-free abelian group, a nonzero integer multiple vanishes only on zero.

theorem IntegralLattice.eq_zero_of_two_zsmul_eq_zero {Λ : Type u_1} [AddCommGroup Λ] [NoZeroSMulDivisors ℤ Λ] {x : Λ} (h : 2 • x = 0) : x = 0

2 • x = 0 → x = 0.

This is the article's §8 step "2[E] = 0 in a torsion-free lattice, hence [E] = 0" — the smallest genuinely load-bearing target in the registry.

theorem IntegralLattice.zsmul_injective {Λ : Type u_1} [AddCommGroup Λ] [NoZeroSMulDivisors ℤ Λ] {n : ℤ} (hn : n ≠ 0) : Function.Injective fun (x : Λ) => n • x

Scaling by a nonzero integer is injective on a torsion-free group.

theorem IntegralLattice.zsmul_left_cancel {Λ : Type u_1} [AddCommGroup Λ] [NoZeroSMulDivisors ℤ Λ] {n : ℤ} (hn : n ≠ 0) {x y : Λ} (h : n • x = n • y) : x = y

Cancellation: n • x = n • y → x = y for n ≠ 0.