Smooth projective congruence classes give simultaneous divisors for homogeneous evaluation matrices.

At a nonsingular reduced point the translated hypersurface equation has multiplicity one.

theorem CCDN.smooth_projective_hypersurface_congruence_minorGcd {p n s N d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → IntPoint (n + 3)) (k : Fin (n + 3)) (a : Fin (n + 2) → ℤ) (ha : MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin (n + 2)) => ↑(a j)) (projectiveHypersurfaceChart k f) = 0) (hs : ∃ (j : Fin (n + 2)), (MvPolynomial.eval fun (i : Fin (n + 2)) => ↑(a i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (projectiveHypersurfaceChart k f))) ≠ 0) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i k)) (hres : ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ z i ((Equiv.swap 0 k) j.succ) - a j * z i k) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : ↑p ^ hypersurfaceMultiplicityExponent (n + 1) 1 s ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

If integer zeros z i of a homogeneous f all have their k-th coordinate prime to p and reduce, in the affine chart k, to the same nonsingular point a of f mod p, then for forms F j of a common degree M the power p ^ hypersurfaceMultiplicityExponent (n + 1) 1 s divides the gcd of the maximal minors of the evaluation matrix (F j (z i)).