fg_def — Mathlib

English

A subfield S is finitely generated over F iff there exists a finite set t ⊆ E with adjoin F t = S.

Русский

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

LaTeX

$$$S.FG \iff \exists t : Set E, Set.Finite t \land adjoin F t = S$$$

Lean4

theorem fg_def {S : IntermediateField F E} : S.FG ↔ ∃ t : Set E, Set.Finite t ∧ adjoin F t = S :=
  Iff.symm Set.exists_finite_iff_finset

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