separable_of_subsingleton — Mathlib

English

If the base ring R is a Subsingleton, then every polynomial in R[X] is separable.

Русский

Если база R является подсобственностью (Subsingleton), то каждый многочлен в R[X] разделим.

LaTeX

$$$[\\text{Subsingleton } R] \\Rightarrow \\forall f \\in R[X], \\operatorname{Separable}(f)$$$

Lean4

@[nontriviality]
theorem separable_of_subsingleton [Subsingleton R] (f : R[X]) : f.Separable := by
  simp [Separable, IsCoprime, eq_iff_true_of_subsingleton]

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