instLattice — Mathlib

English

The collection of finite Galois intermediate fields forms a lattice, with join and meet operations induced from the underlying lattice structure of intermediate fields.

Русский

Множество конечных Галуа-подполей образует решётку; операции объединения и пересечения в этой решётке соответствуют соответствующим операциями в основании — промежуточных полях.

LaTeX

$$$ \text{FiniteGaloisIntermediateField}(k,K) \text{ is a lattice, with } L_1 \lor L_2 \text{ and } L_1 \land L_2 \text{ given by } (L_1.toIntermediateField \sqcup L_2.toIntermediateField), (L_1.toIntermediateField \sqcap L_2.toIntermediateField). $$$

Lean4

instance : Lattice (FiniteGaloisIntermediateField k K) :=
  val_injective.lattice _ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

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