mem_mk — Mathlib

English

For s a Subsemiring of L with hK ensuring the algebra map from K lands in s, and hi a compatibility condition, x ∈ IntermediateField.mk (Subalgebra.mk s hK) hi iff x ∈ s.

Русский

Пусть s — подполье L, такая что образ K в L лежит в s, и hi совместимость. Тогда x ∈ IntermediateField.mk (Subalgebra.mk s hK) hi тогда и только тогда, когда x ∈ s.

LaTeX

$$$x \in \operatorname{IntermediateField.mk}(\operatorname{Subalgebra.mk}(s,h_K),\, hi) \iff x \in s$$$

Lean4

@[simp]
theorem mem_mk (s : Subsemiring L) (hK : ∀ x, algebraMap K L x ∈ s) (hi) (x : L) :
    x ∈ IntermediateField.mk (Subalgebra.mk s hK) hi ↔ x ∈ s :=
  Iff.rfl

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