Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_single_one_mul

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) (r : k) (x : G), (SkewMonoidAlgebra.single 1 r * f).coeff x = r * f.coeff x

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMonoidMulSemiringAction