algebraMap_apply — Mathlib

English

Let S be an intermediate field of L over K. The algebra map from S to L acts as the identity on S, i.e., for all x ∈ S, algebraMap S L x = x.

Русский

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

LaTeX

$$$\\text{algebraMap}_{S,L}(x) = x \\quad (x \\in S)$$$

Lean4

@[simp]
theorem algebraMap_apply (x : S) : algebraMap S L x = x :=
  rfl

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