separable_def — Mathlib

English

Let f be a polynomial over a commutative semiring R. Then f is separable over R if and only if f and its derivative are coprime.

Русский

Пусть f — полином над коммутативной полукольцом R. Тогда f разложим над R тогда и только тогда, когда f и его производная взаимно неприводимы.

LaTeX

$$$ f.Separable \iff \operatorname{IsCoprime}(f, \operatorname{derivative} f) $$$

Lean4

theorem separable_def (f : R[X]) : f.Separable ↔ IsCoprime f (derivative f) :=
  Iff.rfl

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