Theorems · Theorem · ring theory

SkewMonoidAlgebra.mapDomain_smul

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {f : G → G'} {v : SkewMonoidAlgebra k G}
  {R : Type u_5} [inst_1 : Monoid R] [inst_2 : DistribMulAction R k] {b : R},
  (SkewMonoidAlgebra.mapDomain f) (b • v) = b • (SkewMonoidAlgebra.mapDomain f) v

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidMonoidDistribMulAction