coe_toIntermediateField — Mathlib

English

The underlying set of the intermediate field obtained from a subfield is exactly the original subfield.

Русский

Множество, лежащее в основе промежуточного поля, полученного из подполе, совпадает с исходным подполем.

LaTeX

$$$((S.toIntermediateField(\\text{algebra\_map\_mem})) : \\mathrm{Set}\\,L) = S$$$

Lean4

@[simp]
theorem coe_toIntermediateField (S : Subfield L) (algebra_map_mem : ∀ x, (algebraMap K L) x ∈ S) :
    ((S.toIntermediateField algebra_map_mem) : Set L) = S :=
  rfl

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