Theorems · Theorem · ring theory

MonoidAlgebra.counitAlgHom_comp_mapRingHom

∀ {R : Type u_1} {S : Type u_2} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommMonoid M]
  (f : R →+* S),
  (Bialgebra.counitAlgHom S (MonoidAlgebra S M)).comp (MonoidAlgebra.mapRingHom M f) =
    f.comp (Bialgebra.counitAlgHom R (MonoidAlgebra R M)).toRingHom

Defined in

Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommMonoid