imCLM_coe — Mathlib

English

The coe of imCLM to a linear map equals imLm; the two views agree as linear maps.

Русский

Связующее отображение imCLM к линейному отображению равняется imLm; обе реализации совпадают.

LaTeX

$$$(\text{imCLM} : \text{StrongDual } \mathbb{R} K) : K \to_{\mathbb{R}} \mathbb{R} = \text{imLm}$$$

Lean4

@[simp, rclike_simps, norm_cast]
theorem imCLM_coe : ((imCLM : StrongDual ℝ K) : K →ₗ[ℝ] ℝ) = imLm :=
  rfl

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