Theorems · Theorem

MonoidHom.toAdditiveRight_apply_apply

∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (a : Multiplicative α →* β) (a_1 : α),
  (MonoidHom.toAdditiveRight a) a_1 = Additive.ofMul (a (Multiplicative.ofAdd a_1))

Defined in

Mathlib.Algebra.Group.TypeTags.Hom

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses Quot.sound

Assumes

AddZeroClassMulOneClass