toSubalgebra_toIntermediateField'

English

Let S be a subalgebra of L that is a field. Then the intermediate-field obtained from S, via the canonical construction, has S as its underlying subalgebra.

Русский

Пусть S — подалгебра L, являющийся полем. Тогда промежуточное поле, полученное из S указанной конструкцией, имеет в качестве подалгебры именно S.

LaTeX

$$$\\big(S^{\\text{toIntermediateField}'(h_S)}\\big)^{\\text{toSubalgebra}} = S$$$

Lean4

@[simp]
theorem toSubalgebra_toIntermediateField' (S : Subalgebra K L) (hS : IsField S) :
    (S.toIntermediateField' hS).toSubalgebra = S := by
  ext
  rfl

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