fg_adjoin_of_finite

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

If t is finite, then adjoin F t is finitely generated.

Русский

Если t конечное, то adjoin_F t конечнопорождаемо.

LaTeX

$$$t\text{ finite} \Rightarrow (\operatorname{adjoin}_F t) .FG$$$

Lean4

theorem fg_adjoin_of_finite {t : Set E} (h : Set.Finite t) : (adjoin F t).FG :=
  fg_def.mpr ⟨t, h, rfl⟩

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

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

Разделы

Аффилиация

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