unitization_algebraMap — Mathlib

English

For r ∈ 𝕜, the composed embeddings agree: the image of algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A)) r under ofLp equals the image under algebraMap 𝕜 (Unitization 𝕜 A) r.

Русский

Для элемента r ∈ 𝕜 отображение через algebraMap согласуется: образ algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A)) r через ofLp совпадает с образцом algebraMap 𝕜 (Unitization 𝕜 A) r.

LaTeX

$$$ofLp (algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A)) r) = algebraMap 𝕜 (Unitization 𝕜 A) r$$$

Lean4

@[simp]
theorem unitization_algebraMap (r : 𝕜) :
    ofLp (algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A)) r) = algebraMap 𝕜 (Unitization 𝕜 A) r :=
  rfl

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