Theorems · Theorem · ring theory

SkewMonoidAlgebra.lift_single

∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k] (F : G →* A) (a : G) (b : k),
  ((SkewMonoidAlgebra.lift k G A) F) (SkewMonoidAlgebra.single a b) = b • F a

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Lift

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringMonoidSemiringAlgebraMulSemiringActionSMulCommClass