Theorems · Definition

AddMonoidHom.toMultiplicative

{α : Type u_3} →
  {β : Type u_4} →
    [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) ≃ (Multiplicative α →* Multiplicative β)

Reinterpret α →+ β as Multiplicative α →* Multiplicative β.

Defined in

Mathlib.Algebra.Group.TypeTags.Hom

Cited by

21 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

AddZeroClassAddZeroClass