Theorems · Theorem · ring theory

SkewMonoidAlgebra.mapDomain_comp

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {G'' : Type u_4} {f : G → G'} {g : G' → G''}
  {v : SkewMonoidAlgebra k G},
  (SkewMonoidAlgebra.mapDomain (g ∘ f)) v = (SkewMonoidAlgebra.mapDomain g) ((SkewMonoidAlgebra.mapDomain f) v)

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoid