instMul

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

Lean4

/-- The product of `f g : SkewMonoidAlgebra k G` is the finitely supported function whose value
  at `a` is the sum of `f x * (x • g y)` over all pairs `x, y` such that `x * y = a`.
  (Think of a skew group ring.) -/
instance : Mul (SkewMonoidAlgebra k G) :=
  ⟨fun f g ↦ f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * (a₁ • b₂))⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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