instFiniteDimensionalSubtypeMemIntermediateField

Mathlib.FieldTheory.Galois.GaloisClosure

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

English

If L2 is finite-dimensional over k, then L1 ∩ L2 is finite-dimensional over k.

Русский

Если L2 конечномерно над k, то L1 ∩ L2 также конечномерно над k.

LaTeX

$$If $L_2$ is finite dimensional over $k$, then $\dim_k(L_1 \cap L_2) < \infty$.$$

Lean4

instance (L : FiniteGaloisIntermediateField k K) : FiniteDimensional k L :=
  L.finiteDimensional

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

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

Разделы

Аффилиация

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