instIsGaloisSubtypeMemIntermediateFieldMax

English

If L1 and L2 are Galois over k, then the intermediate field corresponding to their join L1 ⊔ L2 is Galois over k.

Русский

Если L1 и L2 галуа над k, то галуа-расширение над k для объединения L1 и L2 сохраняется.

LaTeX

$$If IsGalois(k, L1) and IsGalois(k, L2) then IsGalois(k, ↑(L1 ⊔ L2)).$$

Lean4

/-- Turns the collection of finite Galois IntermediateFields of `K/k` into a lattice. -/
instance (L₁ L₂ : IntermediateField k K) [IsGalois k L₁] [IsGalois k L₂] : IsGalois k ↑(L₁ ⊔ L₂) where

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