adjoin — Mathlib

English

adjoin F S is the smallest intermediate field of E containing the image of F and the set S.

Русский

adjoin F S — наименьшее промежуточное поле под E, содержащее образ F и множество S.

LaTeX

$$\operatorname{adjoin}_F S = \text{Subfield.closure} (\operatorname{range}(\operatorname{algebraMap} F E) \cup S)$$

Lean4

/-- `adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`. -/
@[stacks 09FZ "first part"]
def adjoin : IntermediateField F E :=
  { Subfield.closure (Set.range (algebraMap F E) ∪ S) with
    algebraMap_mem' := fun x => Subfield.subset_closure (Or.inl (Set.mem_range_self x)) }

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