isPurelyInseparable_tower_bot — Mathlib

English

If a subalgebra L of E is both purely inseparable and separable over F, then L = F.

Русский

Если подалгебра L внутри E является одновременно чисто безразделимой и сепарабельной над F, то L = F.

LaTeX

$$$ (L : Subalgebra F E) \; [IsPurelyInseparable F L] [Algebra.IsSeparable F L] \Rightarrow L = ⊥ $$$

Lean4

instance isPurelyInseparable_tower_bot [IsPurelyInseparable F K] : IsPurelyInseparable F M :=
  IsPurelyInseparable.tower_bot F M K

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