instIsSeparableSubtypeMemIntermediateFieldMin

English

If L1,L2 are intermediate fields and L2 is separable over k, then L1 ∩ L2 is separable over k.

Русский

Если L1,L2 — промежуточные поля и L2 сепарабельное над k, то L1 ∩ L2 сепарабельно над k.

LaTeX

$$If IsSeparable k (Subtype {x | x ∈ L2}) then IsSeparable k (Subtype {x | x ∈ L1 ∩ L2}).$$

Lean4

instance (L₁ L₂ : IntermediateField k K) [Algebra.IsSeparable k L₁] : Algebra.IsSeparable k ↑(L₁ ⊓ L₂) :=
  .of_algHom _ _ (IntermediateField.inclusion inf_le_left)

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