content of finsupp

Stream: maths

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

Oh, that doesn't exist

[Johan Commelin]

docs#free_abelian_group

[Eric Wieser]

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

[Johan Commelin]

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]

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

[Ruben Van de Velde]

Does https://leanprover-community.github.io/mathlib_docs/data/finset/gcd.html help?

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

Hmm, I guess that would work!

[Johan Commelin]

Hmm :sad: now I need: ⊢ gcd_monoid ℤ

[Anne Baanen]

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

[Johan Commelin]

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