mem_subalgebraEquivIntermediateField

English

Let L be algebraic over K. For every subalgebra S ⊆ L over K, the intermediate field corresponding to S has exactly the same elements as S; i.e. membership coincides under the natural correspondence.

Русский

Пусть L над K алгебраически расширяется. Для любого подполья S ⊆ L над K соответствующее промежуточное поле содержит ровно те же элементы, что и S; членство совпадает под естественным соответствием.

LaTeX

$$$\forall x \in L,\ x \in \mathcal{I}(S) \iff x \in S$$$

Lean4

@[simp]
theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L} {x : L} :
    x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
  Iff.rfl

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