Gcd type tags

Stream: Is there code for X?

[Aaron Anderson]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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

[Aaron Anderson]

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]

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]

@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]

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]

@Heather Macbeth thank you!

[Aaron Anderson]

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]

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