pairwise_coprime_X_sub_C — Mathlib

English

Let K be a field and s: I → K be injective. Then the family {X − C(s(i))} is pairwise coprime in K[X].

Русский

Пусть K — поле, и s: I → K инъективно. Тогда множество {X − C(s(i))} попарно неприводимо в K[X].

LaTeX

$$For a field K and an injection s: I → K, we have Pairwise IsCoprime on the family (X − C(s(i))).$$

Lean4

theorem pairwise_coprime_X_sub_C {K} [Field K] {I : Type v} {s : I → K} (H : Function.Injective s) :
    Pairwise (IsCoprime on fun i : I => X - C (s i)) := fun _ _ hij =>
  isCoprime_X_sub_C_of_isUnit_sub (sub_ne_zero_of_ne <| H.ne hij).isUnit

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