separable_def' — Mathlib

English

Let R be a commutative semiring and f be a polynomial in R[X]. Then f is separable if and only if there exist polynomials a,b ∈ R[X] such that a f + b f' = 1, where f' denotes the derivative of f.

Русский

Пусть R — коммутативное полукольцо и f ∈ R[X]. Тогда f является разделимым тогда и только тогда, когда существуют полиномы a,b ∈ R[X], такие что a f + b f' = 1, где f' обозначает производную f.

LaTeX

$$$\\\\operatorname{Separable}(f) \\\\\\iff \\\\exists a,b \in R[X],\\\\ a f + b f' = 1$$$

Lean4

theorem separable_def' (f : R[X]) : f.Separable ↔ ∃ a b : R[X], a * f + b * (derivative f) = 1 :=
  Iff.rfl

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