instIsGaloisSubtypeMemIntermediateFieldMin

Mathlib.FieldTheory.Galois.GaloisClosure

URI: https://scilib.ai/kg/mathlib#FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin

English

If L1,L2 are IsGalois over k, then the subtype corresponding to their meet L1 ⊓ L2 is IsGalois over k.

Русский

Если L1 и L2 — галуа над k, то пересечение L1 ⊓ L2 — галуа над k.

LaTeX

$$IsGalois k (Subtype fun x => SetLike.instMembership.mem (SemilatticeInf.toMin.min L1 L2) x).$$

Lean4

instance (L₁ L₂ : IntermediateField k K) [IsGalois k L₁] [IsGalois k L₂] : IsGalois k ↑(L₁ ⊓ L₂) where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru