algebraMap_toProd — Mathlib

English

The algebra map from 𝕜 into 𝓜(𝕜,A) corresponds under toProd to the pair of algebra maps on endomorphisms.

Русский

Алгебраическое отображение из 𝕜 в 𝓜(𝕜,A) под отображением toProd переходит в пару алгебраических отображений на эндоморфизмах.

LaTeX

$$$ (\\mathrm{algebraMap}_{𝕜}(\\mathcal{M}(\\mathbb{K},A))\\ k).toProd = (\\mathrm{algebraMap}_{𝕜}(End(A))\\ k, \\mathrm{algebraMap}_{𝕜}(End(A))\\ k)$$$

Lean4

@[simp]
theorem algebraMap_toProd (k : 𝕜) : (algebraMap 𝕜 𝓜(𝕜, A) k).toProd = algebraMap 𝕜 _ k :=
  rfl

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