toIntermediateField_toSubfield — Mathlib

English

For any intermediate field S of L over K, converting it back to a Subfield via toSubfield recovers S.

Русский

Для любого промежуточного поля S над K в L обратное преобразование к Subfield восстанавливает S.

LaTeX

$$$\\big(S.toIntermediateField(\\text{algebra\_map\_mem})\\big).toSubfield = S$$$

Lean4

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

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