rank_adjoin_eq_one_iff — Mathlib

English

For any set S of elements of E, the rank of the field generated by S over F is 1 exactly when S is contained in the base field.

Русский

Для множества элементов S ⊆ E ранг поля, порожденного F и S, равен 1 тогда, когда S ⊆ F.

LaTeX

$$$\operatorname{rank}_F(\operatorname{adjoin} F S) = 1 \;\iff\; S \subseteq (\perp : \text{IntermediateField } F E)$$$

Lean4

theorem rank_adjoin_eq_one_iff : Module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) :=
  Iff.trans rank_eq_one_iff adjoin_eq_bot_iff

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