Vantieghem's primality criterion: the ∏(2^k−1) form fails at n=2

The commonly quoted Vantieghem criterion 'n prime iff ∏_{k=1}^{n-1}(2^k−1) ≡ n mod 2^n−1' is false for n = 2 (product 1, not ≡ 2 mod 3). The correct all-n≥2 form uses ∏(1−2^k); the two agree for odd n. In Lean the prime direction is short: prove ∏_{k∈Ico 1 p}(1−ζ^k) = p for a primitive root (X_pow_sub_one_eq_prod, image of ζ^· over range p via eq_of_subset_of_card_le, cancel X−1, eval at 1), then minpoly.isIntegrallyClosed_dvd plus cyclotomic_eq_minpoly gives Φ_p ∣ ∏(1−X^k) − p in ℤ[X], and Polynomial.eval_dvd at X=2 with cyclotomic_prime gives 2^p−1. Composite direction: d = n / minFac n, 2^d−1 divides n, Nat.minFac_sq_le_self gives n ≤ d², so d ≤ 4; then interval_cases d and omega.