Theorems · Theorem · ring theory

SkewMonoidAlgebra.mapDomain_mul

∀ {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [inst : Semiring β] [inst_1 : Monoid α]
  [inst_2 : Monoid α₂] [inst_3 : FunLike F α α₂] [inst_4 : MulSemiringAction α β] [inst_5 : MulSemiringAction α₂ β]
  [MulHomClass F α α₂] {f : F} (x y : SkewMonoidAlgebra β α),
  (∀ (a : α) (x : β), a • x = f a • x) →
    (SkewMonoidAlgebra.mapDomain ⇑f) (x * y) = (SkewMonoidAlgebra.mapDomain ⇑f) x * (SkewMonoidAlgebra.mapDomain ⇑f) y

Like mapDomain_add, but for the skewed convolutive multiplication we define in this file. This theorem holds assuming that (hf : ∀ (a : α) (x : β), a • x = (f a) • x).

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMonoidMonoidFunLikeMulSemiringActionMulSemiringActionMulHomClass