isSeparable_tower_bot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance isSeparable_tower_bot [Algebra.IsSeparable F K] : Algebra.IsSeparable F M :=
  Algebra.isSeparable_tower_bot_of_isSeparable F M K

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