Format probe s1
ProvedTaoFivePrimes.zz_probe_s1probe
Probe: trivial identity importing the Type II bridge theorem module, to validate the import path. To be deprecated.
Preamble
import Mathlib import Theorems.Thm_TaoFivePrimes_theorem51TypeII_eq_norm_eta0VaughanBilinearSum
Formal statement
theorem TaoFivePrimes.zz_probe_s1 (n : ℕ) : n = n := by sorry