instIsSeparableSubtypeMemIntermediateFieldMin_1

English

If L1,L2 are intermediate fields and L2 is separable, then the intersection field inherits separability structure.

Русский

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

LaTeX

$$IsSeparable k (Subtype fun x => SetLike.instMembership.mem (L1 ∩ L2) x).$$

Lean4

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

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