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

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

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

@Manuel Eberl thanks. A useful command!

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

I was used to the panel in jEdit, but sometimes I run `Find Theorems`

there and it doesn't seem to stop.

That's odd, I never encountered that.

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

Last updated: Dec 07 2023 at 16:21 UTC