Theorems · Theorem · number theory
Int.gcd_eq_gcd_ab
∀ (x y : ℤ), ↑(x.gcd y) = x * x.gcdA y + y * x.gcdB y
Bézout's lemma
- Defined in
- Mathlib.Data.Int.GCD
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.gcdAproof · cited by 23
- Nat.gcdBproof · cited by 21
- Nat.gcd_eq_gcd_abproof · cited by 13
- Int.gcdAstatement and proof · cited by 7
- Int.gcdBstatement and proof · cited by 7
Cited by6
Results whose statement or proof uses this declaration.
- Int.isCoprime_iff_gcd_eq_oneproof · cited by 16
- Int.gcd_dvd_iffproof · cited by 3
- Int.dvd_of_dvd_mul_left_of_gcd_oneproof · cited by 1
- Int.closure_eq_zmultiplesproof · cited by 0
- Int.isCoprime_gcdAproof · cited by 0
- Int.isCoprime_gcdBproof · cited by 0