Stream: Is there code for X?

Topic: Euclid's lemma


view this post on Zulip Anthony Bordg (Apr 15 2021 at 17:36):

Do we have Euclid's lemma? If so, where?

Euclid's lemma: if abca \mid bc and (a,b)=1(a,b) = 1, then aca \mid c.

view this post on Zulip Manuel Eberl (Apr 15 2021 at 18:33):

This is easily found with find_theorems:

find_theorems "coprime" "_ dvd _ * _"

  GCD.semiring_gcd_class.coprime_dvd_mult_left_iff:
    coprime ?a ?c  (?a dvd ?b * ?c) = (?a dvd ?b)
  GCD.semiring_gcd_class.coprime_dvd_mult_right_iff:
    coprime ?a ?c  (?a dvd ?c * ?b) = (?a dvd ?b)

view this post on Zulip Anthony Bordg (Apr 19 2021 at 09:31):

@Manuel Eberl thanks. A useful command!

view this post on Zulip Manuel Eberl (Apr 19 2021 at 09:33):

You can also equivalently use the ‘Find Theorems’ panel in jEdit. And there's also https://search.isabelle.in.tum.de by @Fabian Huch , which I still haven't used (alas).

view this post on Zulip Anthony Bordg (Apr 19 2021 at 10:00):

I was used to the panel in jEdit, but sometimes I run Find Theorems there and it doesn't seem to stop.

view this post on Zulip Manuel Eberl (Apr 19 2021 at 10:02):

That's odd, I never encountered that.

view this post on Zulip Mathias Fleury (Apr 19 2021 at 10:32):

I have. Usually, the rest of Isabelle is not responsive either during those times.


Last updated: Jun 22 2021 at 07:00 UTC