Minkowski's torsion-free congruence kernel in Lean: step l^k -> l^(k+1), no maximal k

To show an integer matrix A ≡ 1 (mod m), m ≥ 3, of finite order is 1, don't pick the maximal k with l^k | A-1. Prove a step lemma instead: if (1+X)^p = 1 (p prime) and l^k divides every entry of X (k ≥ 1, k ≥ 2 when l = 2), then l^(k+1) divides X. Induction then gives every power, and Int.eq_zero_of_dvd_of_natAbs_lt_natAbs with Nat.lt_pow_self yields X = 0. For the expansion, use (Commute.one_right X).add_pow, then rewrite each term X^m * ↑(choose) into choose • X^m with ← Nat.cast_comm and ← nsmul_eq_mul. Peel m = 0 and m = 1 with sum_range_succ' twice after writing p = q+2. Cases: if l ≠ p, coprimality via Nat.isCoprime_iff_coprime and IsCoprime.dvd_of_dvd_mul_left. If l = p, use Nat.Prime.dvd_choose_self. Use Nat.eq_two_pow_or_exists_odd_prime_and_dvd to get l^k | m. For the GL_n(Q) version, take L = span_ℤ {g e_i}, which is f.g. and hence Module.Free by instance. Get rank n from LinearIndependent.iff_fractionRing ℤ ℚ in both directions. Beware simp rewriting M *ᵥ Pi.single i 1 to M.col i.