Two-entry integer tuples

Arithmetic of Fin 2 → ℤ. Nothing here involves matrices; the results are stated for tuples so that callers holding a diagonal, a pair of invariant factors, or any other two integers can use them without dragging in linear algebra.

Main results

• Int.eq_of_dvd_of_dvd_of_mul_eq_mul: two tuples with positive, mutually dividing first entries and equal products are equal.

Provenance

Adapted from AINTLIB (Chris Birkbeck), Apache-2.0, at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, from LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean. The source's snf_mutual_dvd_eq draws the same conclusion from Smith-normal-form data and routes through smith_normal_form_unique; Int.eq_of_dvd_of_dvd_of_mul_eq_mul keeps none of those matrix hypotheses and does not use it.

theorem Int.eq_of_dvd_of_dvd_of_mul_eq_mul {a b : Fin 2 → ℤ} (ha0_pos : 0 < a 0) (hb0_pos : 0 < b 0) (hab : a 0 ∣ b 0) (hba : b 0 ∣ a 0) (hprod : a 0 * a 1 = b 0 * b 1) : a = b

Two Fin 2 → ℤ tuples with positive, mutually dividing first entries and equal products are equal. The first entries agree by antisymmetry of divisibility among positives, and the second is then pinned by cancelling the first out of the product.

Only the first entries are assumed positive; the second may be negative or zero.