Theorems · Definition · number theory
Int.gcdA
ℤ → ℤ → ℤ
The extended GCD a value in the equation gcd x y = x * a + y * b.
- Defined in
- Mathlib.Data.Int.GCD
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.gcdAproof · cited by 23
Cited by7
Results whose statement or proof uses this declaration.
- Int.isCoprime_iff_gcd_eq_oneproof · cited by 16
- Int.gcd_eq_gcd_abstatement and proof · cited by 6
- 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_gcdAstatement and proof · cited by 0
- Int.isCoprime_gcdBproof · cited by 0