map — Mathlib

English

If E / L / F is a tower of extensions and x ∈ E is separable over F, then x is separable over L as well.

Русский

Если E/ L/ F — каскад расширений и x ∈ E раздeляем над F, то x также раздельно над L.

LaTeX

$$IsSeparable F x → IsSeparable L x$$

Lean4

theorem map [Ring L] [Algebra F L] {x : K} (f : K →ₐ[F] L) (hf : Function.Injective f) (H : IsSeparable F x) :
    IsSeparable F (f x) := by rwa [IsSeparable, minpoly.algHom_eq _ hf]

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