instIsGaloisSubtypeMemIntermediateField

Mathlib.FieldTheory.Galois.GaloisClosure

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

English

If L1 and L2 are both Galois over k, then their intersection L1 ∩ L2 is also Galois over k.

Русский

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

LaTeX

$$If $L_1,L_2$ are IsGalois over $k$, then $\mathrm{IsGalois}(k, L_1 \cap L_2)$.$$

Lean4

instance (L : FiniteGaloisIntermediateField k K) : IsGalois k L :=
  L.isGalois

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

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

Разделы

Аффилиация

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