def Hex.DensePoly.Coprime {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p q : DensePoly K) : Prop

A Bézout identity witnesses coprimality without storing a gcd.

Equations

• p.Coprime q = ∃ (s : Hex.DensePoly K), ∃ (t : Hex.DensePoly K), s * p + t * q = 1

theorem Hex.DensePoly.monic_one {K : Type u} [Lean.Grind.Field K] [DecidableEq K] : Monic 1

The constant polynomial one is monic.

theorem Hex.DensePoly.mul_right_cancel {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {a b c : DensePoly K} (hc : c ≠ 0) (h : a * c = b * c) : a = b

Multiplication by a nonzero polynomial is injective.

theorem Hex.DensePoly.mul_ne_zero {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q : DensePoly K} (hp : p ≠ 0) (hq : q ≠ 0) : p * q ≠ 0

A product of nonzero polynomials over a field is nonzero.

theorem Hex.DensePoly.leadingCoeff_ne_zero {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p : DensePoly K} (hp : p ≠ 0) : p.leadingCoeff ≠ 0

A nonzero polynomial has a nonzero leading coefficient.

theorem Hex.DensePoly.scale_one {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p : DensePoly K) : scale 1 p = p

Scaling by one leaves a polynomial unchanged.

theorem Hex.DensePoly.scale_eq_C_mul {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (a : K) (p : DensePoly K) : scale a p = C a * p

Scaling is multiplication by the corresponding constant polynomial.

theorem Hex.DensePoly.monicize_eq_scale {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p : DensePoly K) : p.monicize = scale p.leadingCoeff⁻¹ p

Monic normalization is scalar multiplication, including at zero.

theorem Hex.DensePoly.bezout_monicize_gcd {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p q : DensePoly K) : ∃ (s : DensePoly K), ∃ (t : DensePoly K), s * p + t * q = (p.gcd q).monicize

The monic gcd admits Bézout coefficients.

theorem Hex.DensePoly.gcd_ne_zero_right {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p q : DensePoly K) (hq : q ≠ 0) : p.gcd q ≠ 0

A gcd with a nonzero right input is nonzero.

theorem Hex.DensePoly.coprime_iff {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p q : DensePoly K) : p.Coprime q ↔ (p.gcd q).monicize = 1

Coprimality is equivalent to the canonical gcd being one.

theorem Hex.DensePoly.Coprime.one_right {K : Type u} [Lean.Grind.Field K] [DecidableEq K] (p : DensePoly K) : p.Coprime 1

Every polynomial is coprime to one.

theorem Hex.DensePoly.Coprime.symm {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q : DensePoly K} (h : p.Coprime q) : q.Coprime p

Coprimality is symmetric.

theorem Hex.DensePoly.Coprime.dvd_one {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q d : DensePoly K} (h : p.Coprime q) (hp : d ∣ p) (hq : d ∣ q) : d ∣ 1

A common divisor of coprime polynomials divides one.

theorem Hex.DensePoly.Coprime.dvd_of_dvd_mul {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q r : DensePoly K} (h : p.Coprime q) (hd : q ∣ p * r) : q ∣ r

A factor coprime to a divisor can be cancelled from a divisibility claim.

theorem Hex.DensePoly.Coprime.of_dvd_right {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q d : DensePoly K} (h : p.Coprime q) (hd : d ∣ q) : p.Coprime d

Coprimality passes to a divisor of the right operand.

theorem Hex.DensePoly.Coprime.mul_right {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q r : DensePoly K} (hq : p.Coprime q) (hr : p.Coprime r) : p.Coprime (q * r)

Coprimality is preserved by products in the right operand.

theorem Hex.DensePoly.Coprime.add_mul {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q r : DensePoly K} (h : p.Coprime q) : (p + r * q).Coprime q

Adding a multiple of the right operand preserves coprimality.

theorem Hex.DensePoly.Coprime.scale_left {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q : DensePoly K} (h : p.Coprime q) {a : K} (ha : a ≠ 0) : (scale a p).Coprime q

Scaling either operand by a nonzero field scalar preserves coprimality.

theorem Hex.DensePoly.coprime_cofactors {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q d a b : DensePoly K} (hd : d ≠ 0) (hp : p = d * a) (hq : q = d * b) (hbez : ∃ (s : DensePoly K), ∃ (t : DensePoly K), s * p + t * q = d) : a.Coprime b

Cancelling a common factor from its Bézout identity yields coprime cofactors.

theorem Hex.DensePoly.monic_of_mul {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q : DensePoly K} (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic

A monic factor of a monic product has a monic cofactor.

theorem Hex.DensePoly.dvd_trans {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q r : DensePoly K} (hpq : p ∣ q) (hqr : q ∣ r) : p ∣ r

Divisibility is transitive.

theorem Hex.DensePoly.Coprime.of_dvd {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q a b : DensePoly K} (h : p.Coprime q) (ha : a ∣ p) (hb : b ∣ q) : a.Coprime b

Coprimality passes to divisors in both operands.

theorem Hex.DensePoly.Coprime.mul {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {a b c d : DensePoly K} (hac : a.Coprime c) (had : a.Coprime d) (hbc : b.Coprime c) (hbd : b.Coprime d) : (a * b).Coprime (c * d)

Two products are coprime when each pair of factors is coprime.

theorem Hex.DensePoly.monic_pow {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p : DensePoly K} (hp : p.Monic) (n : Nat) : (p ^ n).Monic

Powers of monic polynomials remain monic.

theorem Hex.DensePoly.Coprime.pow_right {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q : DensePoly K} (h : p.Coprime q) (n : Nat) : p.Coprime (q ^ n)

Coprimality is preserved under powers of the right operand.

theorem Hex.DensePoly.Coprime.pow {K : Type u} [Lean.Grind.Field K] [DecidableEq K] {p q : DensePoly K} (h : p.Coprime q) (m n : Nat) : (p ^ m).Coprime (q ^ n)

Powers of coprime polynomials are coprime.