# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Gcd type tags

#### 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?

#### 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.

#### 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?

#### 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.

#### 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"?

#### 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)

#### 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?

#### 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

#### 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.

#### 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:

#### 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.

#### Riccardo Brasca (Sep 21 2020 at 19:11):

@Heather Macbeth thank you!

#### 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

#### 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