coe_algebraMap — Mathlib

English

The evaluation at x ∈ α of the algebra map from K to α → β agrees with evaluating the algebra map to α → β pointwise; i.e., for k ∈ K and x ∈ α, (algebraMap K (α → β) k)(x) = algebraMap K β k.

Русский

Проверяется согласованность канонического отображения алгебры: для любого k ∈ K и x ∈ α выполняется (algebraMap K (α → β) k)(x) = algebraMap K β k.

LaTeX

$$$\\bigl(\\mathrm{algebraMap}_K^{\\alpha \\to \\beta}(k)\\bigr)(x) = \\mathrm{algebraMap}_K^{\\beta}(k).$$$

Lean4

@[simp]
theorem coe_algebraMap [CommSemiring K] [Semiring β] [Algebra K β] (k : K) (x : α) :
    ⇑(algebraMap K (α →ₛ β)) k x = algebraMap K (α → β) k x :=
  rfl

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