val — Mathlib

English

The embedding from an intermediate field S of L into L is the natural inclusion map; i.e., S.val is the canonical K-algebra embedding into L.

Русский

Встраивание S в L как подполе является естественным включением; S.val — каноническое K-алгебраическое вложение в L.

LaTeX

$$$ \\operatorname{val} : S \\to_K L \\,;\\; \\operatorname{val}(s) = s \\quad (s \\in S) $$$

Lean4

/-- The embedding from an intermediate field of `L / K` to `L`. -/
def val : S →ₐ[K] L :=
  S.toSubalgebra.val

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