FG — Mathlib · SciLib

English

A subfield S is finitely generated over F if there exists a finite set t of elements of E such that adjoin F t equals S.

Русский

Подполе S над F может быть конечна порождено: существует конечный набор элементов t ⊆ E, такой что adjoin_F t = S.

LaTeX

$$$S.FG \iff \exists t : Set E, \ Set.Finite t \land \operatorname{adjoin}_F t = S$$$

Lean4

/-- An intermediate field `S` is finitely generated if there exists `t : Finset E` such that
`IntermediateField.adjoin F t = S`. -/
@[stacks 09FZ "second part"]
def FG (S : IntermediateField F E) : Prop :=
  ∃ t : Finset E, adjoin F ↑t = S

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