Theorems · Theorem · ring theory

MonoidAlgebra.liftNCRingHom_single

∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Semiring R] (f : k →+* R)
  (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) (a : G) (b : k),
  (MonoidAlgebra.liftNCRingHom f g h_comm) (MonoidAlgebra.single a b) = f b * g a

Defined in

Mathlib.Algebra.MonoidAlgebra.Lift

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMonoidSemiring