coe_toCLM

Mathlib.Topology.Algebra.Module.CharacterSpace

URI: https://scilib.ai/kg/mathlib#WeakDual.CharacterSpace.coe_toCLM

English

The evaluation morphism matches the standard function interpretation.

Русский

Оценочная морфизма совпадает с обычной интерпретацией функции.

LaTeX

$$$\\text{coe}_{toCLM}(φ) = φ$$$

Lean4

@[simp]
theorem coe_toCLM (φ : characterSpace 𝕜 A) : ⇑(toCLM φ) = φ :=
  rfl

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

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

Разделы

Аффилиация

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