def dvd_gcd_all

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/lists.bend:119

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

119# every common divisor of the elements divides gcd_all(xs)   (Mathlib Finset.dvd_gcd)
120def dvd_gcd_all(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: dvd_with(d, xs, ks)) -> {M.gcd_all(xs) == Nat.mul(gw_dvd(xs, ks, 0n, 0n), d) : Nat}:
121  g_dvd(d, xs, ks, 0n, 0n, {==}, h)