Zulip Chat Archive

Stream: maths

Topic: content of finsupp


view this post on Zulip Johan Commelin (Apr 28 2021 at 12:01):

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

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 12:04):

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

view this post on Zulip 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 |-;

view this post on Zulip Eric Wieser (Apr 28 2021 at 12:38):

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

view this post on Zulip Eric Wieser (Apr 28 2021 at 12:38):

Oh, that doesn't exist

view this post on Zulip Johan Commelin (Apr 28 2021 at 12:40):

docs#free_abelian_group

view this post on Zulip Eric Wieser (Apr 28 2021 at 12:43):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 28 2021 at 12:45):

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

view this post on Zulip Ruben Van de Velde (Apr 28 2021 at 12:48):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 28 2021 at 12:50):

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

view this post on Zulip Johan Commelin (Apr 28 2021 at 12:51):

Hmm, I guess that would work!

view this post on Zulip Johan Commelin (Apr 28 2021 at 12:53):

Hmm :sad: now I need: ⊢ gcd_monoid ℤ

view this post on Zulip Anne Baanen (Apr 28 2021 at 12:54):

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

view this post on Zulip 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