Theorems · Theorem

MonoidHom.toAdditive_apply_apply

∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (a : Additive α),
  (MonoidHom.toAdditive f) a = Additive.ofMul (f (Additive.toMul a))

Defined in

Mathlib.Algebra.Group.TypeTags.Hom

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

MulOneClassMulOneClass