of_apply

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.of_apply

English

Applying the embedding, the value at a is the skew basis element: (of k G) a = single a 1.

Русский

Применяя вложение, значение на a равно базисному элементу skew: (of k G) a = single a 1.

LaTeX

$$$(\mathrm{of}\; k\; G)(a) = \mathrm{single}(a,1)$$$

Lean4

@[simp]
theorem of_apply (a : G) : (of k G) a = single a 1 := by simp [of, MonoidHom.coe_mk, OneHom.coe_mk]

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

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

Разделы

Аффилиация

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