apply_at — Mathlib

English

For any x in K, the canonical embedding evaluated at x acts coordinatewise by the embeddings φ: K → ℂ, i.e., (canonicalEmbedding K x)(φ) = φ(x).

Русский

Для любого x в K каноническое вложение действует по координатам: (canonicalEmbedding K x)(φ) = φ(x).

LaTeX

$$$\\forall x\\in K,\\; (\\mathrm{canonicalEmbedding}\\,K\\,x)(\\phi)=\\phi(x)$ for all embeddings φ.$$

Lean4

@[simp]
theorem apply_at (φ : K →+* ℂ) (x : K) : (NumberField.canonicalEmbedding K x) φ = φ x :=
  rfl

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