Theorems · Theorem · number theory
Nat.gcd_eq_gcd_ab
- #60 of the 100 theorems: Bezout’s Theorem
∀ (x y : ℕ), ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
Bézout's lemma: given x y : ℕ, gcd x y = x * a + y * b, where a = gcd_a x y and
b = gcd_b x y are computed by the extended Euclidean algorithm.
- Defined in
- Mathlib.Data.Int.GCD
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_oneproof · cited by 3,885
- add_zeroproof · cited by 2,707
- zero_addproof · cited by 2,366
- Nat.gcdAstatement · cited by 23
- Nat.gcdBstatement · cited by 21
- Nat.xgcdAuxproof · cited by 5
- Nat.xgcd_valproof · cited by 2
- Nat.xgcdAux_valproof · cited by 1
Cited by13
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.pow_of_coprimeproof · cited by 8
- Int.gcd_eq_gcd_abproof · cited by 6
- gcd_nsmul_eq_zeroproof · cited by 3
- ZMod.mul_inv_eq_gcdproof · cited by 3
- PadicInt.norm_sub_modPart_auxproof · cited by 1
- IsUnit.natCast_of_isNilpotent_of_coprimeproof · cited by 1
- CharP.intCast_mul_natCast_gcdA_eq_gcdproof · cited by 1
- Nat.exists_mul_mod_eq_gcdproof · cited by 1
- Commute.pow_eq_pow_iff_of_coprimeproof · cited by 1
- ZMod.eq_unit_mul_divisorproof · cited by 1
- pow_gcd_eq_oneproof · cited by 0
- Int.mod_coprimeproof · cited by 0