instOrderBot — Mathlib

English

There is a bottom element in the lattice FiniteGaloisIntermediateField(k, K); it is given by the finite Galois intermediate field corresponding to the bottom intermediate field.

Русский

В решётке FiniteGaloisIntermediateField(k, K) существует минимальный элемент; он задаётся как минимальное промежуточное поле Галуа.

LaTeX

$$$ \text{bot} := .mk \bot , \; \forall L, \; \text{bot} \le L. $$$

Lean4

instance : OrderBot (FiniteGaloisIntermediateField k K)
    where
  bot := .mk ⊥
  bot_le _ := bot_le (α := IntermediateField _ _)

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