isCoprime_expand — Mathlib

English

If p ≠ 0, then expanding f and g by p preserves coprimality: IsCoprime (expand_R(p,f)) (expand_R(p,g)) ⇔ IsCoprime (f,g).

Русский

Если p ≠ 0, то расширение f и g по p сохраняет взаимопростоту: IsCoprime(expand_R(p,f), expand_R(p,g)) ⇔ IsCoprime(f,g).

LaTeX

$$$$\mathrm{IsCoprime}\bigl(\mathrm{expand}_R(p,f),\ \mathrm{expand}_R(p,g)\bigr) \iff \mathrm{IsCoprime}(f,g)$$$$

Lean4

@[simp]
theorem isCoprime_expand {f g : R[X]} {p : ℕ} (hp : p ≠ 0) : IsCoprime (expand R p f) (expand R p g) ↔ IsCoprime f g :=
  ⟨fun ⟨a, b, eq⟩ ↦
    ⟨contract p a, contract p b, by simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]⟩,
    (·.map _)⟩

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