Theorems · Definition · number theory
Int.gcdB
ℤ → ℤ → ℤ
The extended GCD b 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.gcdBproof · cited by 21
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_gcdAproof · cited by 0
- Int.isCoprime_gcdBstatement and proof · cited by 0