Zulip Chat Archive

Stream: Is there code for X?

Topic: Gcd type tags


view this post on Zulip Aaron Anderson (Sep 21 2020 at 07:12):

Gauss’s lemma (or some version of it) needs a finset/multiset version of gcd. To do this, I could just copy/paste the API from multiset.lattice and finset.lattice, but this seems inefficient. Is there a way to use to_additive or another tactic to streamline this?

view this post on Zulip Aaron Anderson (Sep 21 2020 at 07:17):

If we have a gcd_monoid, to_additive could be a preorder, but you’d need to mod out somehow to turn it directly into a partial-order, and thus a lattice.

view this post on Zulip Aaron Anderson (Sep 21 2020 at 07:18):

A lattice instance on associates would be easy, but how would we translate to that with a tactic?

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 09:56):

This is a great question. We should always push these ideas of two processes being "the same" to a mathematician, to try and make it as transparent as possible in Lean. These are good test cases.

view this post on Zulip Johan Commelin (Sep 21 2020 at 10:07):

Sorry, I'm not sure I follow... can you give an example of a formal statement that you would like to prove "by tactic"?

view this post on Zulip Reid Barton (Sep 21 2020 at 14:18):

Probably stuff like big-gcd of s union t equals the gcd of (big-gcd of s) and (big-gcd of t)

view this post on Zulip Reid Barton (Sep 21 2020 at 14:21):

Maybe we could just declare that the order on associates is given by divisibility (or reverse divisibility?) and work there?

view this post on Zulip Aaron Anderson (Sep 21 2020 at 19:04):

Ideally, we'd translate everything on this page, including what Reid said https://leanprover-community.github.io/mathlib_docs/data/finset/lattice.html

view this post on Zulip Aaron Anderson (Sep 21 2020 at 19:06):

You could possibly get to Gauss's Lemma using only the fact that a constant divides a polynomial if and only if it divides the gcd of the coefficients, which probably just needs the fact that an element divides the gcd of a finset iff it divides all of the elements of the finset.

view this post on Zulip Heather Macbeth (Sep 21 2020 at 19:08):

@Riccardo Brasca I took the liberty of subscribing you to this stream, you might be interested in the discussion of Gauss' lemma :up:

view this post on Zulip Aaron Anderson (Sep 21 2020 at 19:08):

For now, I could probably translate any one result like that one, pretty easily, if I had the lattice structure on associates, which already has the partial order structure. I can start with that PR.

view this post on Zulip Riccardo Brasca (Sep 21 2020 at 19:11):

@Heather Macbeth thank you!

view this post on Zulip Aaron Anderson (Sep 21 2020 at 21:17):

Oh right, the awkward thing is that that lattice structure exists... but only for UFDs... and it's used to build the gcd structure

view this post on Zulip Aaron Anderson (Sep 21 2020 at 21:18):

So this'll need to wait for my UFD refactor to go through


Last updated: May 16 2021 at 05:21 UTC