structure Nat.ExtendedGcdResult : Type

The gcd and the two Bézout coefficients returned by Nat.extendedGcd.

• gcd : Nat

  The greatest common divisor of the inputs.

• coeffA : Int

  The signed coefficient of the first input.

• coeffB : Int

  The signed coefficient of the second input.

@[instance_reducible]

instance Nat.instReprExtendedGcdResult : Repr ExtendedGcdResult

Equations

• Nat.instReprExtendedGcdResult = { reprPrec := Nat.instReprExtendedGcdResult.repr }

def Nat.instReprExtendedGcdResult.repr : ExtendedGcdResult → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Nat.instDecidableEqExtendedGcdResult.decEq (x✝ x✝¹ : ExtendedGcdResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Nat.instDecidableEqExtendedGcdResult : DecidableEq ExtendedGcdResult

Equations

• Nat.instDecidableEqExtendedGcdResult = Nat.instDecidableEqExtendedGcdResult.decEq

@[instance_reducible]

instance Nat.instInhabitedExtendedGcdResult : Inhabited ExtendedGcdResult

Equations

• Nat.instInhabitedExtendedGcdResult = { default := Nat.instInhabitedExtendedGcdResult.default }

@[extern lean_hex_nat_extended_gcd]

def Nat.extendedGcd (a b : Nat) : ExtendedGcdResult

Computes the greatest common divisor of a and b together with signed Bézout coefficients in one pass of the extended Euclidean algorithm. The result r satisfies r.gcd = Nat.gcd a b and (r.gcd : Int) = a * r.coeffA + b * r.coeffB.

For a zero first input, the result is ⟨b, 0, 1⟩, including ⟨0, 0, 1⟩ when both inputs are zero. For a nonzero first input and a zero second input, the result is ⟨a, 1, 0⟩. The coefficients are not unique; no minimality or symmetry of the returned coefficients is specified.

Examples:

• Nat.extendedGcd 240 46 = ⟨2, -9, 47⟩

• Nat.extendedGcd 0 19 = ⟨19, 0, 1⟩

• Nat.extendedGcd 19 0 = ⟨19, 1, 0⟩

Equations

• a.extendedGcd b = Nat.extendedGcd.go a 1 0 b 0 1

@[irreducible]

def Nat.extendedGcd.go (r : Nat) (s t : Int) (r' : Nat) (s' t' : Int) : ExtendedGcdResult

Implementation detail of Nat.extendedGcd: the two rows represent the remainders as linear combinations of the original inputs.

Equations

• Nat.extendedGcd.go r s t r' s' t' = if _h : r = 0 then { gcd := r', coeffA := s', coeffB := t' } else have q := ↑r' / ↑r; Nat.extendedGcd.go (r' % r) (s' - q * s) (t' - q * t) r s t

@[simp]

theorem Nat.extendedGcd_zero_left (b : Nat) : extendedGcd 0 b = { gcd := b, coeffA := 0, coeffB := 1 }

@[simp]

theorem Nat.extendedGcd_zero_right {a : Nat} (h : a ≠ 0) : a.extendedGcd 0 = { gcd := a, coeffA := 1, coeffB := 0 }

@[simp]

theorem Nat.extendedGcd_self {a : Nat} (h : a ≠ 0) : a.extendedGcd a = { gcd := a, coeffA := 1, coeffB := 0 }

@[simp]

theorem Nat.extendedGcd_gcd (a b : Nat) : (a.extendedGcd b).gcd = a.gcd b

The gcd component of Nat.extendedGcd a b is Nat.gcd a b.

theorem Nat.extendedGcd_bezout (a b : Nat) : ↑(a.gcd b) = ↑a * (a.extendedGcd b).coeffA + ↑b * (a.extendedGcd b).coeffB

The coefficients returned by Nat.extendedGcd satisfy Bézout's identity.

theorem Nat.extendedGcd_dvd_left (a b : Nat) : (a.extendedGcd b).gcd ∣ a

The gcd returned by Nat.extendedGcd a b divides a.

theorem Nat.extendedGcd_dvd_right (a b : Nat) : (a.extendedGcd b).gcd ∣ b

The gcd returned by Nat.extendedGcd a b divides b.