Theorems · Theorem · ring theory

AddMonoidAlgebra.liftNC_mul

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

Defined in

Mathlib.Algebra.MonoidAlgebra.Lift

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddSemiringFunLikeMulHomClass