coe_algebraMap_apply — Mathlib

English

Let S be an intermediate field of L over K. For x ∈ K, the base-field algebra map from K to S followed by the inclusion S → L equals the base-field map from K to L directly: algebraMap K S x = algebraMap K L x.

Русский

Пусть S — промежуточное поле L над K. Для x ∈ K отображение алгебраического отображения из K в S, затем включение S → L, совпадает с прямым отображением из K в L: algebraMap K S x = algebraMap K L x.

LaTeX

$$$\\uparrow(\\text{algebraMap}_{K,S} x) = \\text{algebraMap}_{K,L} x$$$

Lean4

@[simp]
theorem coe_algebraMap_apply (x : K) : ↑(algebraMap K S x) = algebraMap K L x :=
  rfl

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