coe_toContinuousLinearMap — Mathlib

English

The evaluation of the continuous-linear map obtained from an algebra homomorphism coincides with the original map.

Русский

Понижение к непрерывному линейному отображению конгруентно исходному гомоморфизму.

LaTeX

$$$\\big(\\varphi^{\\text{toContinuousLinearMap}}\\big) = \\varphi$$$

Lean4

@[simp]
theorem coe_toContinuousLinearMap (φ : A →ₐ[𝕜] 𝕜) : ⇑φ.toContinuousLinearMap = φ :=
  rfl

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