rep_unique
plain-language theorem explainer
Multiplication by a nonzero integer δ is cancellative in ℤ. Constructions of quantized subgroups cite this result to guarantee unique coefficients for each group element. The tactic proof rewrites the equality to obtain a product equal to zero, invokes the no-zero-divisors theorem mul_eq_zero, and discards the δ = 0 case to conclude n equals m.
Claim. For integers $δ, n, m$ with $δ ≠ 0$, if $n δ = m δ$ then $n = m$.
background
The module LedgerUnits studies the subgroup of integers generated by a fixed nonzero δ, denoted DeltaSub δ, whose elements are precisely the multiples kδ for k in ℤ. The module documentation notes that this subgroup specializes to a clean order isomorphism when δ equals 1. The lemma depends on mul_eq_zero from IntegersFromLogic, which asserts that the logic integers have no zero divisors because of their isomorphism to the standard integers.
proof idea
The proof first uses sub_mul to show that (n - m) δ equals zero. It then applies mul_eq_zero to deduce that n - m equals zero or δ equals zero. The second alternative is ruled out by the assumption δ ≠ 0, and sub_eq_zero finishes the argument that n equals m.
why it matters
The result provides the uniqueness half of the bijection between ℤ and the δ-subgroup. It is used in the quantization theorem, which states that every element of DeltaSub δ has a unique integer coefficient, and in the lemma toZ_fromZ to verify that the maps are inverses. Within the Recognition framework this step supports the construction of ledger units from the integer logic, feeding into the forcing chain toward physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.