instMin — Mathlib

English

In the lattice FiniteGaloisIntermediateField(k, K), the greatest lower bound (infimum) of two finite Galois intermediate fields L1 and L2 corresponds to the intersection of their underlying intermediate fields.

Русский

В решётке FiniteGaloisIntermediateField(k, K) наибольшая нижняя граница двух Галуа-подполей L1 и L2 соответствует пересечению их базовых промежуточных полей.

LaTeX

$$$ (\min(L_1,L_2)).toIntermediateField = L_1.toIntermediateField \sqcap L_2.toIntermediateField $$$

Lean4

instance : Min (FiniteGaloisIntermediateField k K) where min L₁ L₂ := .mk <| L₁ ⊓ L₂

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