Gcd of a set of natural numbers or integers

Stream: Is there code for X?

[Alex J. Best]

I have a possibly infinite set of integers (or naturals), that I'd like to take the GCD of.
What is the best way to do this (i.e. most available lemmas) with mathlib currently?
My best attempt so far is to take the generator of the integer ideal generated by the set using docs#submodule.is_principal.generator. But something that uses the normalization gcd monoid stucture sounds better (so that the gcd is positive), is there such an instance using Sup already?

[Eric Wieser]

I guess you want a type alias that defines sup = gcd?

[Eric Wieser]

Which came up before in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Gcd.20type.20tags/near/210707674

[Alex J. Best]

Yeah I thought associates would be the right thing, which in the case of nat is an equivalent type. But a type alias might be the right answer in general