Theorems · Theorem · ring theory

SkewMonoidAlgebra.liftNC_single

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {R : Type u_5} [inst_1 : NonUnitalNonAssocSemiring R]
  (f : k →+ R) (g : G → R) (a : G) (b : k), (SkewMonoidAlgebra.liftNC f g) (SkewMonoidAlgebra.single a b) = f b * g a

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommMonoidNonUnitalNonAssocSemiring