English
Let k ⊆ K be fields and consider the finite Galois intermediate fields FiniteGaloisIntermediateField(k, K). For any two such fields L1 and L2, their least upper bound in this lattice is the finite Galois intermediate field whose underlying intermediate field is the join of the underlying intermediate fields L1 and L2.
Русский
Пусть k ⊆ K — поля, и рассмотрим множество конечных Галуа-подполей FiniteGaloisIntermediateField(k, K). Для любых двух таких полей L1, L2 их наименьшее верхнее множество в этой решётке равно конечному Галуа-подполю, чья сопряжённая промежуточная область имеет основание L1 ⊔ L2.
LaTeX
$$$ (\max(L_1,L_2)).toIntermediateField = L_1.toIntermediateField \sqcup L_2.toIntermediateField $$$
Lean4
instance : Max (FiniteGaloisIntermediateField k K) where max L₁ L₂ := .mk <| L₁ ⊔ L₂
