Theory BatchKZG_poly_bind

theory BatchKZG_poly_bind

imports BatchKZG_def KZG_poly_bind

begin

section ‹Polynomial Binding of the batched KZG›

locale BatchEvalKZG_PCS_poly_bind = BatchEvalKZG + KZG_CS_binding
begin

text ‹We inherit polynomial binding for the batched KZG directly from the standard KZG.›
theorem "bKZG.poly_bind_advantage 𝒜 ≤ t_DL_G⇩p.advantage (bind_reduction 𝒜)"
  using polynomial_binding by blast

end

end