Transport algebra morphisms between additive and multiplicative types.

def AddMonoidHom.toMultiplicative {α : Type u_3} {β : Type u_4} [AddZeroClass α] [AddZeroClass β] : (α →+ β) ≃ (Multiplicative α →* Multiplicative β)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidHom.toMultiplicative_apply_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (a : Multiplicative α) : (toMultiplicative f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))

@[simp]

theorem AddMonoidHom.toMultiplicative_symm_apply_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [AddZeroClass β] (f : Multiplicative α →* Multiplicative β) (a : α) : (toMultiplicative.symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

@[simp]

theorem AddMonoidHom.coe_toMultiplicative {α : Type u_3} {β : Type u_4} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) : ⇑(toMultiplicative f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Multiplicative.toAdd

@[simp]

theorem AddMonoidHom.toMultiplicative_id {α : Type u_3} [AddZeroClass α] : toMultiplicative (id α) = MonoidHom.id (Multiplicative α)

def MonoidHom.toAdditive {α : Type u_3} {β : Type u_4} [MulOneClass α] [MulOneClass β] : (α →* β) ≃ (Additive α →+ Additive β)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem MonoidHom.toAdditive_symm_apply_apply {α : Type u_3} {β : Type u_4} [MulOneClass α] [MulOneClass β] (f : Additive α →+ Additive β) (a : α) : (toAdditive.symm f) a = Additive.toMul (f (Additive.ofMul a))

@[simp]

theorem MonoidHom.coe_toAdditive {α : Type u_3} {β : Type u_4} [MulOneClass α] [MulOneClass β] (f : α →* β) : ⇑(toAdditive f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Additive.toMul

@[deprecated MonoidHom.coe_toAdditive (since := "2025-11-07")]

theorem MonoidHom.coe_toMultiplicative {α : Type u_3} {β : Type u_4} [MulOneClass α] [MulOneClass β] (f : α →* β) : ⇑(toAdditive f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Additive.toMul

Alias of MonoidHom.coe_toAdditive.

@[simp]

theorem MonoidHom.toAdditive_id {α : Type u_3} [MulOneClass α] : toAdditive (id α) = AddMonoidHom.id (Additive α)

def AddMonoidHom.toMultiplicativeRight {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] : (Additive α →+ β) ≃ (α →* Multiplicative β)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidHom.toMultiplicativeRight_apply_apply {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) (a : α) : (toMultiplicativeRight f) a = Multiplicative.ofAdd (f (Additive.ofMul a))

@[simp]

theorem AddMonoidHom.toMultiplicativeRight_symm_apply_apply {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) (a : Additive α) : (toMultiplicativeRight.symm f) a = Multiplicative.toAdd (f (Additive.toMul a))

@[deprecated AddMonoidHom.toMultiplicativeRight (since := "2025-09-19")]

def AddMonoidHom.toMultiplicative' {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] : (Additive α →+ β) ≃ (α →* Multiplicative β)

Alias of AddMonoidHom.toMultiplicativeRight.

---

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

Equations

• @AddMonoidHom.toMultiplicative' = @AddMonoidHom.toMultiplicativeRight

@[simp]

theorem AddMonoidHom.coe_toMultiplicativeRight {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) : ⇑(toMultiplicativeRight f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul

@[deprecated AddMonoidHom.coe_toMultiplicativeRight (since := "2025-09-19")]

theorem AddMonoidHom.coe_toMultiplicative' {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) : ⇑(toMultiplicativeRight f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul

Alias of AddMonoidHom.coe_toMultiplicativeRight.

def MonoidHom.toAdditiveLeft {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] : (α →* Multiplicative β) ≃ (Additive α →+ β)

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

Equations

• MonoidHom.toAdditiveLeft = AddMonoidHom.toMultiplicativeRight.symm

@[simp]

theorem MonoidHom.toAdditiveLeft_symm_apply_apply {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (a✝ : Additive α →+ β) (a : α) : (toAdditiveLeft.symm a✝) a = Multiplicative.ofAdd (a✝ (Additive.ofMul a))

@[simp]

theorem MonoidHom.toAdditiveLeft_apply_apply {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (a✝ : α →* Multiplicative β) (a : Additive α) : (toAdditiveLeft a✝) a = Multiplicative.toAdd (a✝ (Additive.toMul a))

@[deprecated MonoidHom.toAdditiveLeft (since := "2025-09-19")]

def MonoidHom.toAdditive' {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] : (α →* Multiplicative β) ≃ (Additive α →+ β)

Alias of MonoidHom.toAdditiveLeft.

---

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

Equations

• @MonoidHom.toAdditive' = @MonoidHom.toAdditiveLeft

@[simp]

theorem MonoidHom.coe_toAdditiveLeft {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) : ⇑(toAdditiveLeft f) = ⇑Multiplicative.toAdd ∘ ⇑f ∘ ⇑Additive.toMul

@[deprecated MonoidHom.coe_toAdditiveLeft (since := "2025-09-19")]

theorem MonoidHom.coe_toAdditive' {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) : ⇑(toAdditiveLeft f) = ⇑Multiplicative.toAdd ∘ ⇑f ∘ ⇑Additive.toMul

Alias of MonoidHom.coe_toAdditiveLeft.

def AddMonoidHom.toMultiplicativeLeft {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] : (α →+ Additive β) ≃ (Multiplicative α →* β)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidHom.toMultiplicativeLeft_apply_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) (a : Multiplicative α) : (toMultiplicativeLeft f) a = Additive.toMul (f (Multiplicative.toAdd a))

@[simp]

theorem AddMonoidHom.toMultiplicativeLeft_symm_apply_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) (a : α) : (toMultiplicativeLeft.symm f) a = Additive.ofMul (f (Multiplicative.ofAdd a))

@[deprecated AddMonoidHom.toMultiplicativeLeft (since := "2025-09-19")]

def AddMonoidHom.toMultiplicative'' {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] : (α →+ Additive β) ≃ (Multiplicative α →* β)

Alias of AddMonoidHom.toMultiplicativeLeft.

---

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

Equations

• @AddMonoidHom.toMultiplicative'' = @AddMonoidHom.toMultiplicativeLeft

@[simp]

theorem AddMonoidHom.coe_toMultiplicativeLeft {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) : ⇑(toMultiplicativeLeft f) = ⇑Additive.toMul ∘ ⇑f ∘ ⇑Multiplicative.toAdd

@[deprecated AddMonoidHom.coe_toMultiplicativeLeft (since := "2025-09-19")]

theorem AddMonoidHom.coe_toMultiplicative'' {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) : ⇑(toMultiplicativeLeft f) = ⇑Additive.toMul ∘ ⇑f ∘ ⇑Multiplicative.toAdd

Alias of AddMonoidHom.coe_toMultiplicativeLeft.

def MonoidHom.toAdditiveRight {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] : (Multiplicative α →* β) ≃ (α →+ Additive β)

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

Equations

• MonoidHom.toAdditiveRight = AddMonoidHom.toMultiplicativeLeft.symm

@[simp]

theorem MonoidHom.toAdditiveRight_symm_apply_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (a✝ : α →+ Additive β) (a : Multiplicative α) : (toAdditiveRight.symm a✝) a = Additive.toMul (a✝ (Multiplicative.toAdd a))

@[simp]

theorem MonoidHom.toAdditiveRight_apply_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (a✝ : Multiplicative α →* β) (a : α) : (toAdditiveRight a✝) a = Additive.ofMul (a✝ (Multiplicative.ofAdd a))

@[deprecated MonoidHom.toAdditiveRight (since := "2025-09-19")]

def MonoidHom.toAdditive'' {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] : (Multiplicative α →* β) ≃ (α →+ Additive β)

Alias of MonoidHom.toAdditiveRight.

---

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

Equations

• @MonoidHom.toAdditive'' = @MonoidHom.toAdditiveRight

@[simp]

theorem MonoidHom.coe_toAdditiveRight {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) : ⇑(toAdditiveRight f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Multiplicative.ofAdd

@[deprecated MonoidHom.coe_toAdditiveRight (since := "2025-09-19")]

theorem MonoidHom.coe_toAdditive'' {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) : ⇑(toAdditiveRight f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Multiplicative.ofAdd

Alias of MonoidHom.coe_toAdditiveRight.

theorem Multiplicative.monoidHom_ext {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] (f g : Multiplicative α →* β) (h : MonoidHom.toAdditiveRight f = MonoidHom.toAdditiveRight g) : f = g

This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.

WARNING: This has the potential to send ext into a loop if someone locally adds the inverse ext lemma proving equality in α →+ Additive β from equality in Multiplicative α →* β.

theorem Multiplicative.monoidHom_ext_iff {α : Type u_3} {β : Type u_4} [AddZeroClass α] [MulOneClass β] {f g : Multiplicative α →* β} : f = g ↔ MonoidHom.toAdditiveRight f = MonoidHom.toAdditiveRight g

theorem Additive.addMonoidHom_ext {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] (f g : Additive α →+ β) (h : AddMonoidHom.toMultiplicativeRight f = AddMonoidHom.toMultiplicativeRight g) : f = g

This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.

WARNING: This has the potential to send ext into a loop if someone locally adds the inverse ext lemma proving equality in α →* Multiplicative β from equality in Additive α →+ β.

theorem Additive.addMonoidHom_ext_iff {α : Type u_3} {β : Type u_4} [MulOneClass α] [AddZeroClass β] {f g : Additive α →+ β} : f = g ↔ AddMonoidHom.toMultiplicativeRight f = AddMonoidHom.toMultiplicativeRight g

@[simp]

theorem AddMonoidHom.toMultiplicative_add {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddCommMonoid N] (f g : M →+ N) : toMultiplicative (f + g) = toMultiplicative f * toMultiplicative g

def AddMonoidHom.toMultiplicativeLeftAddEquiv {M : Type u_1} {N : Type u_2} [AddMonoid M] [CommMonoid N] : (M →+ Additive N) ≃+ Additive (Multiplicative M →* N)

AddMonoidHom.toMultiplicativeLeft as an AddEquiv.

Equations

• AddMonoidHom.toMultiplicativeLeftAddEquiv = { toEquiv := AddMonoidHom.toMultiplicativeLeft.trans Additive.ofMul, map_add' := ⋯ }

def AddMonoidHom.toMultiplicativeRightAddEquiv {M : Type u_1} {N : Type u_2} [Monoid M] [AddCommMonoid N] : (Additive M →+ N) ≃+ Additive (M →* Multiplicative N)

AddMonoidHom.toMultiplicativeRight as an AddEquiv.

Equations

• AddMonoidHom.toMultiplicativeRightAddEquiv = { toEquiv := AddMonoidHom.toMultiplicativeRight.trans Additive.ofMul, map_add' := ⋯ }

def MonoidHom.toAdditiveLeftMulEquiv {M : Type u_1} {N : Type u_2} [Monoid M] [AddCommMonoid N] : (M →* Multiplicative N) ≃* Multiplicative (Additive M →+ N)

MonoidHom.toAdditiveLeft as a MulEquiv.

Equations

• MonoidHom.toAdditiveLeftMulEquiv = { toEquiv := MonoidHom.toAdditiveLeft.trans Multiplicative.ofAdd, map_mul' := ⋯ }

def MonoidHom.toAdditiveRightMulEquiv {M : Type u_1} {N : Type u_2} [AddMonoid M] [CommMonoid N] : (Multiplicative M →* N) ≃* Multiplicative (M →+ Additive N)

MonoidHom.toAdditiveRight as a MulEquiv.

Equations

• MonoidHom.toAdditiveRightMulEquiv = { toEquiv := MonoidHom.toAdditiveRight.trans Multiplicative.ofAdd, map_mul' := ⋯ }