asAlgebraHom_of

Mathlib.RepresentationTheory.Basic

URI: https://scilib.ai/kg/mathlib#Representation.asAlgebraHom_of

English

The image of MonoidAlgebra.of g under asAlgebraHom is ρ(g).

Русский

Образ MonoidAlgebra.of g под asAlgebraHom равен ρ(g).

LaTeX

$$asAlgebraHom ρ (MonoidAlgebra.of k G g) = ρ g$$

Lean4

theorem asAlgebraHom_of (g : G) : asAlgebraHom ρ (of k G g) = ρ g := by
  simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul]

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

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

Разделы

Аффилиация

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