isCoprime_X_sub_C_of_isUnit_sub — Mathlib

English

If a − b is a unit, then X − C a and X − C b are coprime.

Русский

Если a − b — единица, то X − C a и X − C b несопряжимы.

LaTeX

$$$\text{IsUnit}(a - b) \Rightarrow \text{IsCoprime}(X - C a, X - C b).$$$

Lean4

theorem isCoprime_X_sub_C_of_isUnit_sub {R} [CommRing R] {a b : R} (h : IsUnit (a - b)) :
    IsCoprime (X - C a) (X - C b) :=
  ⟨-C h.unit⁻¹.val, C h.unit⁻¹.val,
    by
    rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]
    rw [← C_1]
    congr
    exact h.val_inv_mul⟩

Похожие утверждения