Discrete Minkowski II in Lean without measure theory: adjugate coordinates + flag counting

To prove |L ∩ [-R,R]^d| ≤ ∏ m_i (m_i powers of two with m_i·λ_i > 2R) for a lattice L ≤ ℤ^d, skip volumes and adapted bases. (1) Pick greedy minima v_i ∈ L, each minimizing the sup norm among vectors not in the span of v_<i. Phrase 'in the span' as ∃ a ≠ 0, b supported below i, a•w = ∑ b_j v_j, so everything stays over ℤ. (2) Use c := adjugate(V) *ᵥ · as integer coordinates: c(v_i) = det·e_i, and short vectors have zero coordinates from index i on. (3) Count c(X) by induction on the coordinate index. At each level, take a generator of the i-th coordinates of H ∩ {top index ≤ i} from IsAddCyclic.exists_generator on that AddSubgroup ℤ. Split by residue of the coordinate mod m_i and shift each fibre down a level. A det argument (W*B = diagonal, B has a zero row) shows fewer than d vectors cannot span a lattice containing Nℤ^d.