Generic CRT product-basis independence and the unimodularity criterion, Generic independence lemmas reuse LeanPool.Zeta5Irrational; the determinant adapter was copied from Li₂ Li2Unified/Modular/Base/ClassBasis.lean (itself adapted from Apery/Arith/Unimodular.lean in mo271/Zeta5 by Moritz Firsching (https://github.com/mo271/Zeta5, commit f19a1960609f7d38e7b63fd2acb05e6f60a7b741), Apache-2.0), restated for Zeta32.Arith.Local.coeffMat.

theorem Zeta32.PrimeEdge.Auxiliary.coeffMat_det_unit_of_independent {h p : ℕ} [hp : Fact (Nat.Prime p)] (Ez : Fin h → Polynomial ℤ) (hdeg : ∀ (a : Fin h), (Ez a).natDegree < h) (hind : ∀ (v : Fin h → ZMod p), ∑ a : Fin h, Polynomial.C (v a) * Polynomial.map (Int.castRingHom (ZMod p)) (Ez a) = 0 → v = 0) : (Arith.Local.coeffMat fun (a : Fin h) => Polynomial.map (Int.castRingHom ℚ) (Ez a)).det ≠ 0 ∧ padicValRat p (Arith.Local.coeffMat fun (a : Fin h) => Polynomial.map (Int.castRingHom ℚ) (Ez a)).det = 0

A polynomial family independent modulo p has a p-unit coefficient determinant.