isSeparable_mul — Mathlib

English

If E/F is separable, finSepDegree F E = finrank F E.

Русский

Если расширение E/F сепарабельно, то finSepDegree F E = finrank F E.

LaTeX

$$$ finSepDegree F E = finrank F E $$$

Lean4

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

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