toIntermediateField'_toSubalgebra

English

Let S be an intermediate field of L over K. The subalgebra obtained from S via toSubalgebra is exactly S.

Русский

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

LaTeX

$$$S_{\\toSubalgebra} = S$ (where $S_{\\toSubalgebra}$ denotes $(S.toSubalgebra)^{\\text{IntermediateField}}$)$$

Lean4

@[simp]
theorem toIntermediateField'_toSubalgebra (S : IntermediateField K L) :
    S.toSubalgebra.toIntermediateField' (Field.toIsField S) = S :=
  by
  ext
  rfl

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