isSeparable_neg — Mathlib

English

If x and y are separable over F, then their sum x + y is separable over F.

Русский

Если x и y сепарабельны над F, то их сумма x + y сепарабельна над F.

LaTeX

$$$ IsSeparable F x \to IsSeparable F y \to IsSeparable F (x + y) $$$

Lean4

/-- If `x` is a separable elements, then `-x` is also a separable element. -/
theorem isSeparable_neg {x : E} (hx : IsSeparable F x) : IsSeparable F (-x) :=
  haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).2 hx
  isSeparable_of_mem_isSeparable F E <| F⟮x⟯.neg_mem <| mem_adjoin_simple_self F x

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