Theory "gcdset"

Parents pred_set gcd

Signature

Constant	Type
gcdset	:(num -> bool) -> num

Definitions

gcdset_def

|- ∀s.
     gcdset s =
     if (s = ∅) ∨ (s = {0}) then 0
     else
       MAX_SET
         ({n | n ≤ MIN_SET (s DELETE 0)} ∩ {d | ∀e. e ∈ s ⇒ divides d e})

Theorems

gcdset_divides

|- ∀e. e ∈ s ⇒ divides (gcdset s) e

gcdset_greatest

|- (∀e. e ∈ s ⇒ divides g e) ⇒ divides g (gcdset s)

gcdset_EMPTY

|- gcdset ∅ = 0

gcdset_INSERT

|- gcdset (x INSERT s) = gcd x (gcdset s)