separable_iff — Mathlib

English

If f and g are associated, then f is separable if and only if g is separable.

Русский

Если f и g ассоциированы, то f разделим тогда и только тогда, когда g разделим.

LaTeX

$$$\\text{Associated}(f,g) \\Rightarrow (\\operatorname{Separable}(f) \\iff \\operatorname{Separable}(g))$$$

Lean4

theorem _root_.Associated.separable_iff {f g : R[X]} (ha : Associated f g) : f.Separable ↔ g.Separable :=
  ⟨ha.separable, ha.symm.separable⟩

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