mem_subalgebraEquivIntermediateField_symm

English

Let L be algebraic over K. For any intermediate field S, and any x ∈ L, we have x ∈ subalgebraEquivIntermediateField.symm S if and only if x ∈ S.

Русский

Пусть L над K алгебраически; для любого промежуточного поля S и любого элемента x ∈ L верно, что x принадлежит subalgebraEquivIntermediateField.symm S тогда и только тогда, когда x ∈ S.

LaTeX

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

Lean4

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

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