Do we have Euclid's lemma? If so, where?
Euclid's lemma: if and , then .
This is easily found with
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