## Stream: maths

### Topic: content of finsupp

#### Johan Commelin (Apr 28 2021 at 12:01):

Do we have anyway of talking about the gcd of a finsupp X int?

#### Kevin Buzzard (Apr 28 2021 at 12:04):

a generator of the ideal generated by the image, you mean?

#### Johan Commelin (Apr 28 2021 at 12:05):

I don't know if literally that is the easiest way of dealing with this in Lean |-;

#### Eric Wieser (Apr 28 2021 at 12:38):

That's the same as docs#free_comm_group, right?

#### Eric Wieser (Apr 28 2021 at 12:38):

Oh, that doesn't exist

#### Johan Commelin (Apr 28 2021 at 12:40):

docs#free_abelian_group

#### Eric Wieser (Apr 28 2021 at 12:43):

Do you mean the gcd under docs#finsupp.has_mul?

#### Johan Commelin (Apr 28 2021 at 12:45):

No, a finsupp X int is basically just a list of integers (indexed by some finset in X) and I want the gcd of those integers.

#### Johan Commelin (Apr 28 2021 at 12:45):

So the gcd will be an int, not a finsupp X int

#### Eric Wieser (Apr 28 2021 at 12:49):

Can gcd be spelt with infi somehow? If so, that sounds like \Inf (i : f.support), f i

#### Eric Wieser (Apr 28 2021 at 12:50):

So (f.support.image f).gcd?

#### Johan Commelin (Apr 28 2021 at 12:51):

Hmm, I guess that would work!

#### Johan Commelin (Apr 28 2021 at 12:53):

Hmm :sad: now I need: ⊢ gcd_monoid ℤ

#### Anne Baanen (Apr 28 2021 at 12:54):

That should be in src/ring_theory/int/basic.lean

#### Johan Commelin (Apr 28 2021 at 12:56):

Great: this works: let d : ℤ := (N.support.gcd N),

Last updated: Jun 17 2021 at 16:20 UTC