structure Hex.DensePoly.GcdStep (F : Type u) [Zero F] [DecidableEq F] : Type u

A two-by-two polynomial transformation, kept local to fast gcd rather than introducing a dependency on the matrix library.

• a00 : DensePoly F

  Upper-left matrix entry.

• a01 : DensePoly F

  Upper-right matrix entry.

• a10 : DensePoly F

  Lower-left matrix entry.

• a11 : DensePoly F

  Lower-right matrix entry.

def Hex.DensePoly.GcdStep.det {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m : GcdStep F) : DensePoly F

Determinant of a polynomial transformation.

Equations

• m.det = m.a00 * m.a11 - m.a01 * m.a10

def Hex.DensePoly.GcdStep.one {F : Type u} [DecidableEq F] [Lean.Grind.Field F] : GcdStep F

Identity transformation.

Equations

• Hex.DensePoly.GcdStep.one = { a00 := 1, a01 := 0, a10 := 0, a11 := 1 }

def Hex.DensePoly.GcdStep.euclid {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (q : DensePoly F) : GcdStep F

One Euclidean transformation (a,b) ↦ (b,a-q*b).

Equations

• Hex.DensePoly.GcdStep.euclid q = { a00 := 0, a01 := 1, a10 := 1, a11 := -q }

def Hex.DensePoly.GcdStep.compose {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m n : GcdStep F) : GcdStep F

Matrix composition; compose m n applies n first and then m.

Equations

• m.compose n = { a00 := m.a00 * n.a00 + m.a01 * n.a10, a01 := m.a00 * n.a01 + m.a01 * n.a11, a10 := m.a10 * n.a00 + m.a11 * n.a10, a11 := m.a10 * n.a01 + m.a11 * n.a11 }

@[simp]

theorem Hex.DensePoly.GcdStep.det_one {F : Type u} [DecidableEq F] [Lean.Grind.Field F] : one.det = 1

The identity transformation has determinant one.

@[simp]

theorem Hex.DensePoly.GcdStep.det_euclid {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (q : DensePoly F) : (euclid q).det = -1

A Euclidean row update has determinant negative one.

theorem Hex.DensePoly.GcdStep.det_compose {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m n : GcdStep F) : (m.compose n).det = m.det * n.det

Determinants multiply under transformation composition.

def Hex.DensePoly.GcdStep.composeWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (m n : GcdStep F) : GcdStep F

Plan-driven matrix composition. Half-gcd builds transformations at half the active degree and composes them before touching the full operands.

Equations

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

def Hex.DensePoly.GcdStep.euclidComposeWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (q : DensePoly F) (m : GcdStep F) : GcdStep F

Compose one Euclidean row update with an existing transformation. The elementary matrix contains only zero, one, and -q, so this specialization uses two planned products instead of the eight used by generic composition.

Equations

• Hex.DensePoly.GcdStep.euclidComposeWith plan q m = { a00 := m.a10, a01 := m.a11, a10 := m.a00 + Hex.DensePoly.mulWith plan (-q) m.a10, a11 := m.a01 + Hex.DensePoly.mulWith plan (-q) m.a11 }

def Hex.DensePoly.GcdStep.composeLowWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (len : Nat) (m n : GcdStep F) : GcdStep F

Matrix composition clipped to the coefficient range that can survive in the caller's degree-bounded transformation.

Equations

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

def Hex.DensePoly.GcdStep.apply {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m : GcdStep F) (a b : DensePoly F) : DensePoly F × DensePoly F

Apply a transformation to a polynomial pair.

Equations

• m.apply a b = (m.a00 * a + m.a01 * b, m.a10 * a + m.a11 * b)

@[simp]

theorem Hex.DensePoly.GcdStep.apply_fst {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m : GcdStep F) (a b : DensePoly F) : (m.apply a b).fst = m.a00 * a + m.a01 * b

First row of a polynomial transformation application.

@[simp]

theorem Hex.DensePoly.GcdStep.apply_snd {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m : GcdStep F) (a b : DensePoly F) : (m.apply a b).snd = m.a10 * a + m.a11 * b

Second row of a polynomial transformation application.

def Hex.DensePoly.GcdStep.applyWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (m : GcdStep F) (a b : DensePoly F) : DensePoly F × DensePoly F

Apply a transformation using the selected multiplication plan.

Equations

• Hex.DensePoly.GcdStep.applyWith plan m a b = (Hex.DensePoly.mulWith plan m.a00 a + Hex.DensePoly.mulWith plan m.a01 b, Hex.DensePoly.mulWith plan m.a10 a + Hex.DensePoly.mulWith plan m.a11 b)

def Hex.DensePoly.GcdStep.applyFromHighWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (k : Nat) (m : GcdStep F) (highPair : DensePoly F × DensePoly F) (a b : DensePoly F) : DensePoly F × DensePoly F

Reconstruct a full application from its already-computed high-half application and one application to the low halves. Half-gcd uses this to avoid applying the same recursive matrix to the full operands again.

Equations

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

theorem Hex.DensePoly.GcdStep.composeWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (m n : GcdStep F) : composeWith plan m n = m.compose n

Planned composition has the ordinary matrix semantics.

theorem Hex.DensePoly.GcdStep.euclidComposeWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (q : DensePoly F) (m : GcdStep F) : euclidComposeWith plan q m = composeWith plan (euclid q) m

Specialized Euclidean composition has the generic planned matrix semantics.

theorem Hex.DensePoly.GcdStep.applyWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (m : GcdStep F) (a b : DensePoly F) : applyWith plan m a b = m.apply a b

Planned application has the ordinary matrix semantics.

theorem Hex.DensePoly.GcdStep.composeLowWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (len : Nat) (m n : GcdStep F) (h00 : (m.compose n).a00.size ≤ len) (h01 : (m.compose n).a01.size ≤ len) (h10 : (m.compose n).a10.size ≤ len) (h11 : (m.compose n).a11.size ≤ len) : composeLowWith plan len m n = m.compose n

Clipped matrix composition is ordinary composition once the bound covers all four resulting entries.

@[simp]

theorem Hex.DensePoly.GcdStep.apply_one {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (a b : DensePoly F) : one.apply a b = (a, b)

Identity leaves a pair unchanged.

theorem Hex.DensePoly.GcdStep.apply_euclid {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (q a b : DensePoly F) : (euclid q).apply a b = (b, a - q * b)

The elementary matrix performs exactly one Euclidean update.

theorem Hex.DensePoly.GcdStep.apply_compose {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m n : GcdStep F) (a b : DensePoly F) : (m.compose n).apply a b = m.apply (n.apply a b).fst (n.apply a b).snd

Matrix composition agrees with sequential application.

theorem Hex.DensePoly.GcdStep.ext_apply {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {m n : GcdStep F} (h : ∀ (a b : DensePoly F), m.apply a b = n.apply a b) : m = n

Polynomial-pair action is faithful for two-by-two transformations.

@[simp]

theorem Hex.DensePoly.GcdStep.compose_one {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m : GcdStep F) : m.compose one = m

Identity is a right identity for transformation composition.

@[simp]

theorem Hex.DensePoly.GcdStep.one_compose {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (m : GcdStep F) : one.compose m = m

Identity is a left identity for transformation composition.

def Hex.DensePoly.quotientStep {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (qs : List (DensePoly F)) : GcdStep F

Compose the Euclidean matrices represented by a quotient sequence.

Equations

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

def Hex.DensePoly.runQuotients {F : Type u} [DecidableEq F] [Lean.Grind.Field F] : List (DensePoly F) → DensePoly F → DensePoly F → DensePoly F × DensePoly F

Execute a quotient sequence as ordinary Euclidean pair updates.

Equations

• Hex.DensePoly.runQuotients [] x✝¹ x✝ = (x✝¹, x✝)
• Hex.DensePoly.runQuotients (q :: qs) x✝¹ x✝ = Hex.DensePoly.runQuotients qs x✝ (x✝¹ - q * x✝)

theorem Hex.DensePoly.apply_quotientStep {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (qs : List (DensePoly F)) (a b : DensePoly F) : (quotientStep plan qs).apply a b = runQuotients qs a b

The executable quotient matrix performs exactly the corresponding Euclidean update sequence.

theorem Hex.DensePoly.runQuotients_append {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (qs rs : List (DensePoly F)) (a b : DensePoly F) : runQuotients (qs ++ rs) a b = runQuotients rs (runQuotients qs a b).fst (runQuotients qs a b).snd

Running concatenated quotient blocks is sequential execution.

theorem Hex.DensePoly.quotientStep_append {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (qs rs : List (DensePoly F)) : quotientStep plan (qs ++ rs) = GcdStep.composeWith plan (quotientStep plan rs) (quotientStep plan qs)

Quotient matrices turn list concatenation into matrix composition.

theorem Hex.DensePoly.det_quotientStep {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (qs : List (DensePoly F)) : (quotientStep plan qs).det = 1 ∨ (quotientStep plan qs).det = -1

A quotient transformation is unimodular.

theorem Hex.DensePoly.quotientStep_singleton {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (q : DensePoly F) : quotientStep plan [q] = GcdStep.euclid q

A singleton quotient list is its elementary Euclidean matrix.

inductive Hex.DensePoly.ExactQuotients {F : Type u} [DecidableEq F] [Lean.Grind.Field F] : List (DensePoly F) → DensePoly F → DensePoly F → DensePoly F → DensePoly F → Prop

A quotient sequence is an exact prefix of the established Euclidean sequence, ending at the displayed pair.

• nil {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (a b : DensePoly F) : ExactQuotients [] a b a b
• cons {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {q r a b c d : DensePoly F} {qs : List (DensePoly F)} (hdiv : a.divMod b = (q, r)) (tail : ExactQuotients qs b r c d) : ExactQuotients (q :: qs) a b c d

inductive Hex.DensePoly.ActiveQuotients {F : Type u} [DecidableEq F] [Lean.Grind.Field F] : List (DensePoly F) → DensePoly F → DensePoly F → DensePoly F → DensePoly F → Prop

An exact Euclidean prefix containing only steps at which the divisor is nonzero. This is the executable trace relation: xgcdAux takes precisely these steps and stops before any attempted division by zero.

• nil {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (a b : DensePoly F) : ActiveQuotients [] a b a b
• cons {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {q r a b c d : DensePoly F} {qs : List (DensePoly F)} (hb : 0 < b.size) (hdiv : a.divMod b = (q, r)) (tail : ActiveQuotients qs b r c d) : ActiveQuotients (q :: qs) a b c d

inductive Hex.DensePoly.ProperQuotients {F : Type u} [DecidableEq F] [Lean.Grind.Field F] : List (DensePoly F) → DensePoly F → DensePoly F → DensePoly F → DensePoly F → Prop

An exact Euclidean prefix whose divisors have positive degree and whose quotients are nonzero. These are precisely the steps a half-gcd block may lift from high halves; constant-divisor finishing remains an exact boundary division.

• nil {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (a b : DensePoly F) : ProperQuotients [] a b a b
• cons {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {q r a b c d : DensePoly F} {qs : List (DensePoly F)} (hq : 0 < q.size) (hb : 1 < b.size) (hdiv : a.divMod b = (q, r)) (tail : ProperQuotients qs b r c d) : ProperQuotients (q :: qs) a b c d

theorem Hex.DensePoly.ProperQuotients.exact {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hproper : ProperQuotients qs a b c d) : ExactQuotients qs a b c d

Forgetting the half-gcd degree guards leaves an ordinary exact Euclidean prefix.

theorem Hex.DensePoly.ProperQuotients.active {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hproper : ProperQuotients qs a b c d) : ActiveQuotients qs a b c d

Proper half-gcd steps are active executable Euclidean steps.

theorem Hex.DensePoly.ActiveQuotients.exact {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hactive : ActiveQuotients qs a b c d) : ExactQuotients qs a b c d

Every active trace is an exact Euclidean prefix.

theorem Hex.DensePoly.ProperQuotients.append {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs rs : List (DensePoly F)} {a b c d e f : DensePoly F} (hfirst : ProperQuotients qs a b c d) (hsecond : ProperQuotients rs c d e f) : ProperQuotients (qs ++ rs) a b e f

Concatenating adjacent proper blocks preserves their Euclidean certificate.

theorem Hex.DensePoly.ExactQuotients.append {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs rs : List (DensePoly F)} {a b c d e f : DensePoly F} (hfirst : ExactQuotients qs a b c d) (hsecond : ExactQuotients rs c d e f) : ExactQuotients (qs ++ rs) a b e f

Concatenating adjacent exact Euclidean blocks preserves exactness.

theorem Hex.DensePoly.ActiveQuotients.append {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs rs : List (DensePoly F)} {a b c d e f : DensePoly F} (hfirst : ActiveQuotients qs a b c d) (hsecond : ActiveQuotients rs c d e f) : ActiveQuotients (qs ++ rs) a b e f

Concatenating adjacent active traces preserves executability.

theorem Hex.DensePoly.GcdStep.applyFromHighWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (k : Nat) (matrix : GcdStep F) (a b : DensePoly F) : applyFromHighWith plan k matrix (matrix.apply (high k a) (high k b)) a b = matrix.apply a b

Reusing the exact high-half application preserves ordinary matrix application semantics.

theorem Hex.DensePoly.ExactQuotients.run {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hexact : ExactQuotients qs a b c d) : runQuotients qs a b = (c, d)

Executing an exact prefix reaches its certified terminal pair.

theorem Hex.DensePoly.ExactQuotients.apply {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) {qs : List (DensePoly F)} {a b c d : DensePoly F} (hexact : ExactQuotients qs a b c d) : (quotientStep plan qs).apply a b = (c, d)

Consequently the composed quotient matrix reaches the same certified terminal pair.

structure Hex.DensePoly.GcdBoundaryResult (F : Type u) [Zero F] [DecidableEq F] : Type u

A half-gcd transformation stopped at a requested remainder-size boundary. The displayed pair is cached so callers do not reapply the completed matrix to the full inputs.

• matrix : GcdStep F

  Transformation applied to the input polynomial pair.

• first : DensePoly F

  First polynomial in the transformed pair.

• second : DensePoly F

  Second polynomial in the transformed pair.

@[irreducible]

def Hex.DensePoly.reduceToMatrixResult {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (bound : Nat) : Nat → DensePoly F → DensePoly F → GcdBoundaryResult F

Reduce an ordered Euclidean pair until its second component reaches bound. The shifted high-half call is chosen so that its half-size boundary lifts to bound; when the pair is still much larger, ordinary half-gcd blocks halve it first. Size checks make every high-half prediction untrusted, just as in halfGcdMatrix.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.reduceToMatrixResult plan bound 0 x✝¹ x✝ = { matrix := Hex.DensePoly.GcdStep.one, first := x✝¹, second := x✝ }

theorem Hex.DensePoly.ActiveQuotients.length_le {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hactive : ActiveQuotients qs a b c d) (hd : d = 0) : qs.length ≤ b.size

A complete active Euclidean trace has at most one quotient per stored coefficient of its initial divisor.

theorem Hex.DensePoly.ProperQuotients.terminal_lt {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hproper : ProperQuotients qs a b c d) (hinput : b.size < a.size) : d.size < c.size

Proper Euclidean blocks preserve strict ordering of consecutive remainders.

theorem Hex.DensePoly.ProperQuotients.second_le {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {qs : List (DensePoly F)} {a b c d : DensePoly F} (hproper : ProperQuotients qs a b c d) : d.size ≤ b.size

The second remainder of a proper block never exceeds its second input.

theorem Hex.DensePoly.ProperQuotients.liftHigh {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (k : Nat) {qs : List (DensePoly F)} {ah bh ch dh A B C D : DensePoly F} (hproper : ProperQuotients qs ah bh ch dh) (hrun : runQuotients qs A B = (C, D)) (hcsize : C.size = (shift k ch).size) (hdsize : D.size = (shift k dh).size) : ProperQuotients qs A B C D ∧ A.size = (shift k ah).size ∧ B.size = (shift k bh).size

A proper quotient block computed on high halves lifts to the full inputs once its terminal pair has the shifted high-half sizes. The proof runs the Euclidean recurrence backward: terminal sizes determine the preceding two sizes, making every proposed remainder strictly smaller than its divisor and therefore every quotient exact.

theorem Hex.DensePoly.reduceToMatrixResult_spec {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (bound : Nat) (a b : DensePoly F) (hbound : 0 < bound) (hinput : b.size < a.size) (ha : bound < a.size) : have result := reduceToMatrixResult plan bound b.size a b; result.matrix.apply a b = (result.first, result.second) ∧ result.second.size ≤ bound ∧ bound < result.first.size ∧ 0 < result.matrix.a11.size ∧ result.matrix.a11.size + result.first.size = a.size + 1

The boundary reducer is an exact Euclidean prefix, straddles the requested size, and exposes the complementary continuant size used by rational reconstruction and Padé approximation.

theorem Hex.DensePoly.reduceToMatrixResult_det {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (bound fuel : Nat) (a b : DensePoly F) (hbound : 0 < bound) (hinput : b.size < a.size) : have result := reduceToMatrixResult plan bound fuel a b; result.matrix.det = 1 ∨ result.matrix.det = -1

Every boundary transformation is unimodular.

def Hex.DensePoly.xgcdWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : XGCDResult F

Kernel-visible extended gcd; native code uses the proved half-gcd engine.

Equations

• Hex.DensePoly.xgcdWith plan p q = p.xgcd q

def Hex.DensePoly.gcdWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : DensePoly F

Kernel-visible gcd with exact reference scaling.

Equations

• Hex.DensePoly.gcdWith plan p q = p.gcd q

def Hex.DensePoly.xgcdLeftWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : XGCDLeftResult F

Kernel-visible one-sided extended gcd.

Equations

• Hex.DensePoly.xgcdLeftWith plan p q = p.xgcdLeft q

def Hex.DensePoly.xgcdWithImpl {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : XGCDResult F

Plan-driven half-gcd extended gcd.

Equations

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

def Hex.DensePoly.gcdWithImpl {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : DensePoly F

Gcd projection of the half-gcd engine.

Equations

• Hex.DensePoly.gcdWithImpl plan p q = (Hex.DensePoly.xgcdWithImpl plan p q).gcd

def Hex.DensePoly.xgcdLeftWithImpl {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : XGCDLeftResult F

One-sided result projection of the half-gcd engine. It shares the full matrix computation with xgcdWithImpl; this API omits the unused result field but does not promise a cheaper algorithm.

Equations

• Hex.DensePoly.xgcdLeftWithImpl plan p q = { gcd := (Hex.DensePoly.xgcdWithImpl plan p q).gcd, left := (Hex.DensePoly.xgcdWithImpl plan p q).left }

theorem Hex.DensePoly.xgcdWithImpl_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : xgcdWithImpl plan p q = p.xgcd q

Half-gcd returns exactly the established extended-gcd result, including the raw gcd scaling and both Bezout coefficients.

theorem Hex.DensePoly.gcdWithImpl_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : gcdWithImpl plan p q = p.gcd q

Half-gcd returns exactly the established gcd.

theorem Hex.DensePoly.xgcdLeftWithImpl_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : xgcdLeftWithImpl plan p q = p.xgcdLeft q

The one-sided half-gcd projection agrees exactly with the established one-sided extended gcd.

theorem Hex.DensePoly.xgcdWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : xgcdWith plan p q = p.xgcd q

Planned extended gcd has the exact reference result.

theorem Hex.DensePoly.gcdWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : gcdWith plan p q = p.gcd q

Planned gcd retains the exact reference scaling.

theorem Hex.DensePoly.xgcdLeftWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) : xgcdLeftWith plan p q = p.xgcdLeft q

Planned one-sided extended gcd retains the exact reference result.

@[csimp]

theorem Hex.DensePoly.xgcdWith_csimp : @xgcdWith = @xgcdWithImpl

Compile the extended-gcd reference through the existing half-gcd engine.

@[csimp]

theorem Hex.DensePoly.gcdWith_csimp : @gcdWith = @gcdWithImpl

Compile the gcd reference through the existing half-gcd projection.

@[csimp]

theorem Hex.DensePoly.xgcdLeftWith_csimp : @xgcdLeftWith = @xgcdLeftWithImpl

Compile the one-sided reference through the existing half-gcd projection.