Theorems · Definition · ring theory

SkewMonoidAlgebra.of

(k : Type u_1) →
  (G : Type u_2) →
    [inst : Semiring k] → [inst_1 : Monoid G] → [inst_2 : MulSemiringAction G k] → G →* SkewMonoidAlgebra k G

The embedding of a monoid into its skew monoid algebra.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

15 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringMonoidMulSemiringAction