coe_toNonUnitalAlgHom

Mathlib.Topology.Algebra.Module.CharacterSpace

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

English

The coercion of toNonUnitalAlgHom matches the character-space map.

Русский

Коэрцировка toNonUnitalAlgHom совпадает с отображением пространства характеристик.

LaTeX

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

Lean4

@[simp]
theorem coe_toNonUnitalAlgHom (φ : characterSpace 𝕜 A) : ⇑(toNonUnitalAlgHom φ) = φ :=
  rfl

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

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

Разделы

Аффилиация

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