Theorems · Theorem · ring theory

SkewMonoidAlgebra.lift_symm_apply

∀ {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 : SkewMonoidAlgebra k G →ₐ[k] A) (x : G),
  ((SkewMonoidAlgebra.lift k G A).symm F) x = F (SkewMonoidAlgebra.single x 1)

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Lift

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringMonoidSemiringAlgebraMulSemiringActionSMulCommClass