toIntermediateField — Mathlib

English

From a subalgebra S of L that is closed under inverses, one obtains an intermediate field structure on L with underlying data (S, inv_mem).

Русский

Из подалгебры S L, замкнутой по обратному, получает структуру промежуточного поля на L, заданную данными (S, inv_mem).

LaTeX

$$$\operatorname{toIntermediateField}(S, inv\_mem)$ is an IntermediateField(K,L)$$

Lean4

/-- Turn a subalgebra closed under inverses into an intermediate field. -/
def toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) : IntermediateField K L :=
  { S with inv_mem' := inv_mem }

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