toSubalgebra_toIntermediateField — Mathlib

English

If S is a Subalgebra of L and inv_mem makes S into an intermediate field, then (S.toIntermediateField inv_mem).toSubalgebra = S.

Русский

Если S — подалгебра L и inv_mem делает S промежуточным полем, то (S.toIntermediateField inv_mem).toSubalgebra = S.

LaTeX

$$$\big( S.toIntermediateField\ inv\_mem\big).toSubalgebra = S$$$

Lean4

@[simp]
theorem toSubalgebra_toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
    (S.toIntermediateField inv_mem).toSubalgebra = S := by
  ext
  rfl

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