Stream: Beginner Questions

Topic: gcd

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

Can we find somewhere in Isabelle a version of lemma bezout_gcd_nat (in HOL/Computational_Algebra/Primes) but for integers?

view this post on Zulip Manuel Eberl (Apr 13 2021 at 15:17):

You probably want this from HOL-Computational_Algebra.Euclidean_Algorithm:

lemma bezout_coefficients:
  assumes "bezout_coefficients a b = (x, y)"
  shows "x * a + y * b = gcd a b"

Works for any Euclidean ring.

Last updated: Oct 13 2024 at 01:36 UTC