toIntermediateField_toSubalgebra — Mathlib

English

The intermediate field obtained from a Subalgebra via toIntermediateField and back yields the original Subalgebra: (S.toSubalgebra.toIntermediateField (fun _ => S.inv_mem)) = S.

Русский

Промежуточное поле, полученное из подалгебры через toIntermediateField и обратно, даёт исходную подалгебру: (S.toSubalgebra.toIntermediateField (fun _ => S.inv_mem)) = S.

LaTeX

$$$\big( S.toSubalgebra.toIntermediateField (\text{fun } _ \Rightarrow S.inv\_mem) \big) = S$$$

Lean4

@[simp]
theorem toIntermediateField_toSubalgebra (S : IntermediateField K L) :
    (S.toSubalgebra.toIntermediateField fun _ => S.inv_mem) = S :=
  by
  ext
  rfl

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