Theorems · Theorem · ring theory

MonoidAlgebra.liftNC_mul

∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : Semiring R]
  {g_hom : Type u_6} [inst_3 : FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom)
  (a b : MonoidAlgebra k G),
  (∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)) →
    (MonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (MonoidAlgebra.liftNC ↑f ⇑g) a * (MonoidAlgebra.liftNC ↑f ⇑g) b

Defined in

Mathlib.Algebra.MonoidAlgebra.Lift

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMulSemiringFunLikeMulHomClass