isSeparable_tower_top — Mathlib

English

Let F ⊆ K be fields with M an intermediate field of K over F. If K is separable over F, then K is separable over M.

Русский

Пусть F ⊆ K — поля, и M — промежуточное поле между F и K. Если K separable над F, то K separable над M.

LaTeX

$$$\\operatorname{IsSeparable} F K \\Rightarrow \\forall M : \\text{IntermediateField } F K,\\; \\operatorname{IsSeparable} M K$$$

Lean4

instance isSeparable_tower_top [Algebra.IsSeparable F K] : Algebra.IsSeparable M K :=
  Algebra.isSeparable_tower_top_of_isSeparable F M K

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