finrank_adjoin_eq_one_iff — Mathlib

English

For a set S, finrank F (adjoin F S) = 1 if and only if S is contained in the bottom field.

Русский

Для множества S: финразмерность F(адъюн F S) равна 1 тогда, когда S ⊆ нижнее поле.

LaTeX

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

Lean4

theorem finrank_adjoin_eq_one_iff : finrank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) :=
  Iff.trans finrank_eq_one_iff adjoin_eq_bot_iff

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