coe_eq_algebraMap — Mathlib

English

The natural embedding of 𝕜 into 𝓜(𝕜, 𝕜) given by DoubleCentralizer.coe is the same as the canonical algebra map 𝕜 → 𝓜(𝕜, 𝕜).

Русский

Естественное вложение из 𝕜 в 𝓜(𝕜, 𝕜) через DoubleCentralizer.coe совпадает с каноническим алгебраическим отображением 𝕜 → 𝓜(𝕜, 𝕜).

LaTeX

$$$\text{DoubleCentralizer.coe }\mathbb{K} = \text{algebraMap } \mathbb{K} \; \mathcal{M}(\mathbb{K}, \mathbb{K})$$$

Lean4

theorem coe_eq_algebraMap : (DoubleCentralizer.coe 𝕜 : 𝕜 → 𝓜(𝕜, 𝕜)) = algebraMap 𝕜 𝓜(𝕜, 𝕜) :=
  by
  ext x : 3
  ·
    rfl -- `fst` is defeq

  · refine ContinuousLinearMap.ext fun y => ?_
    exact mul_comm y x

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