inclusion — Mathlib

English

There exists a canonical inclusion map from any E ≤ F between intermediate fields: E →ₐ[K] F, given by inclusion.

Русский

Существует каноническое включение E в F между промежуточными полями: E →ₐ[K] F, задаваемое включением.

LaTeX

$$$\\text{inclusion}_{E\\le F}: E \\to_K F$ with $\\text{inclusion}_{E\\le F}(e)=e$$$

Lean4

/-- The map `E → F` when `E` is an intermediate field contained in the intermediate field `F`.

This is the intermediate field version of `Subalgebra.inclusion`. -/
def inclusion {E F : IntermediateField K L} (hEF : E ≤ F) : E →ₐ[K] F :=
  Subalgebra.inclusion hEF

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