coe_starₗᵢ

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#coe_starₗᵢ

English

The map starₗᵢ 𝕜 coincides with the standard star map on E.

Русский

Отображение starₗᵢ 𝕜 совпадает со стандартной операцией звезды на E.

LaTeX

$$$ (star\_\ell^{\;\mathbb{K}}) = \mathrm{star} $$$

Lean4

@[simp]
theorem coe_starₗᵢ : (starₗᵢ 𝕜 : E → E) = star :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru