Theorems · Theorem · ring theory

AddMonoidAlgebra.liftNC_single

∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : NonUnitalNonAssocSemiring R] (f : k →+ R)
  (g : Multiplicative G → R) (a : G) (b : k),
  (AddMonoidAlgebra.liftNC f g) (AddMonoidAlgebra.single a b) = f b * g (Multiplicative.ofAdd a)

Defined in

Mathlib.Algebra.MonoidAlgebra.Lift

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringNonUnitalNonAssocSemiring