isSeparable_sub — Mathlib

English

If x and y are separable over F, then their difference 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` and `y` are both separable elements, then `x - y` is also a separable element. -/
theorem isSeparable_sub {x y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) : IsSeparable F (x - y) :=
  haveI := isSeparable_adjoin_pair_of_isSeparable F E hx hy
  isSeparable_of_mem_isSeparable F E <| F⟮x, y⟯.sub_mem (subset_adjoin F _ (.inl rfl)) (subset_adjoin F _ (.inr rfl))

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