English
Let p,q ∈ R[X] and r ∈ R be a unit. If p and q are coprime in R[X], then p.scaleRoots(r) and q.scaleRoots(r) are coprime as well.
Русский
Пусть p,q ∈ R[X] и r ∈ R единица. Если p и q взаимно просты в R[X], то и p.scaleRoots(r) и q.scaleRoots(r) взаимно просты.
LaTeX
$$$\\forall R [\\mathrm{CommSemiring}\\ R] (p,q \\in R[X]) (r \\in R^\\times) (h : \\mathrm{IsCoprime}\\ p\\ q),\\; \\mathrm{IsCoprime}(p.scaleRoots(r), q.scaleRoots(r))$$$
Lean4
theorem isCoprime_scaleRoots (p q : R[X]) (r : R) (hr : IsUnit r) (h : IsCoprime p q) :
IsCoprime (p.scaleRoots r) (q.scaleRoots r) :=
by
obtain ⟨a, b, e⟩ := h
let s : R := ↑hr.unit⁻¹
have : natDegree (a * p) = natDegree (b * q) :=
by
apply natDegree_eq_of_natDegree_add_eq_zero
rw [e, natDegree_one]
use s ^ natDegree (a * p) • s ^ (natDegree a + natDegree p - natDegree (a * p)) • a.scaleRoots r
use s ^ natDegree (a * p) • s ^ (natDegree b + natDegree q - natDegree (b * q)) • b.scaleRoots r
simp only [s, smul_mul_assoc, ← mul_scaleRoots, smul_smul, mul_assoc, ← mul_pow, IsUnit.val_inv_mul, one_pow, mul_one,
← smul_add, one_smul, e, natDegree_one, one_scaleRoots, ← add_scaleRoots_of_natDegree_eq _ _ _ this, tsub_zero]
