gcd of a finite set of nats

Stream: Is there code for X?

[Stepan Holub]

I need to work with gcd of a (finite) set or list of natural numbers. Is there already a suitable way to do that without defining it from scratch, like

def gcd_of_list (L : List Nat) : Nat := foldr Nat.gcd 0 L

[Aaron Liu]

docs#Finset.gcd

[Stepan Holub]

Indeed, looks simple. But I am unable to make it work for Nat. The f in the definition

def gcd (s : Finset β) (f : β → α) : α :=
  s.fold GCDMonoid.gcd 0 f

should be identity

fun x => x

I guess. But I am unable to explain to Lean that Nat is an instance of CancelCommMonoidWithZero, NormalizedGCDMonoid.

To start, I would like to get claim of the form

example (s : Finset ℕ) (n : ℕ) (mem: n ∈ s) : Finset.gcd s ∣ n

(the function is missing here, but I am unable to fit anything in)

[Aaron Liu]

Do you have the correct imports?

[Aaron Liu]

#min_imports tells me

import Mathlib.Algebra.GCDMonoid.Finset
import Mathlib.Algebra.GCDMonoid.Nat

[Stepan Holub]

Of course, I tried to make necessary imports. But I was not successful. (That is why I dare to ask the chat.)

[Ruben Van de Velde]

As a tip, you can probably use import Mathlib to be sure you've got everything

[Stepan Holub]

Imported whole mathlib, and writing

example (s : Finset ℕ) (n : ℕ) (mem: n ∈ s) : Finset.gcd (fun x => x) s ∣ n

I get

Application type mismatch: In the application
  Finset.gcd ?m.700 s
the argument
  s
has type
  Finset ℕ : Type
but is expected to have type
  ?m.135 → ℕ : Type (max ?u.132 0)

[Ruben Van de Velde]

The set comes first

[Stepan Holub]

Oops. Yes. That is what the message says. Thank you. Now it is accepted.

[Stepan Holub]

Now it works:

example (s : Finset ℕ) (n : ℕ) (mem: n ∈ s) : Finset.gcd s (fun x => x)  ∣ n := by exact Finset.gcd_dvd mem

Thank both very much.