isSeparable_algebraMap — Mathlib

English

Any element x ∈ F is separable over F after embedding into E.

Русский

Любой элемент x ∈ F сепарабелен над F после вложения в E.

LaTeX

$$$ IsSeparable F x \text{ for } x \in F \text{ via } (algebraMap F E). $$$

Lean4

/-- Any element `x` of `F` is a separable element of `E / F` when embedded into `E`. -/
theorem isSeparable_algebraMap (x : F) : IsSeparable F ((algebraMap F E) x) :=
  by
  rw [IsSeparable, minpoly.algebraMap_eq (algebraMap F E).injective]
  exact Algebra.IsSeparable.isSeparable F x

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