isSeparable_add — Mathlib

English

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

Русский

Если x и y сепарабельны над F, то произведение x y сепарабельно над F.

LaTeX

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

Lean4

/-- If `x` and `y` are both separable elements, then `x + y` is also a separable element. -/
theorem isSeparable_add {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⟯.add_mem (subset_adjoin F _ (.inl rfl)) (subset_adjoin F _ (.inr rfl))

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