instFiniteDimensionalSubtypeMemIntermediateFieldMin

English

Turns the collection of finite Galois IntermediateFields of K/k into a lattice, and preserves finite dimensionality under the infimum operation.

Русский

Преобразование множества конечных галуа-полей K/k в решётку сохраняет конечномерность под операцией infimum.

LaTeX

$$If $L_1,L_2$ are in the finite Galois intermediate fields, then $L_1 \cap L_2$ has finite dimension over k.$$

Lean4

instance (L₁ L₂ : IntermediateField k K) [FiniteDimensional k L₁] : FiniteDimensional k ↑(L₁ ⊓ L₂) :=
  .of_injective (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₁) inf_le_left).toLinearMap
    (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₁) inf_le_left).toRingHom.injective

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