Stream: Is there code for X?

Topic: Euclid's lemma

Anthony Bordg (Apr 15 2021 at 17:36):

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

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

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)

Anthony Bordg (Apr 19 2021 at 09:31):

@Manuel Eberl thanks. A useful command!

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

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.

Manuel Eberl (Apr 19 2021 at 10:02):

That's odd, I never encountered that.

Mathias Fleury (Apr 19 2021 at 10:32):

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

Last updated: Apr 25 2024 at 12:23 UTC