instFiniteDimensionalSubtypeMemIntermediateFieldMin_1

English

If L2 is finite-dimensional, then the intersection dimension statement for Subtype mem L1 ⊓ L2 holds in finite dimension.

Русский

Если L2 конечномерно, то пересечение L1 ∩ L2 имеет конечную размерность, как подтип.

LaTeX

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

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_right).toLinearMap
    (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₂) inf_le_right).injective

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