Theorems · Inductive type · ring theory

SkewMonoidAlgebra

(k : Type u_1) → Type u_2 → [Zero k] → Type (max u_1 u_2)

The skew monoid algebra of G over k is the type of finite formal k-linear combinations of terms of G, endowed with a skewed convolution product.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

216 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Zero