fg_adjoin_finset

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.fg_adjoin_finset

English

If t is a finite set, then the intermediate field generated by t is finitely generated.

Русский

Если t — конечное множество, то подполе, порождаемое t, является конечнопорожденным.

LaTeX

$$$\operatorname{FG}(\operatorname{adjoin}_F t) \,\text{for any finite } t$$$

Lean4

theorem fg_adjoin_finset (t : Finset E) : (adjoin F (↑t : Set E)).FG :=
  ⟨t, rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru