Transport algebra morphisms between additive and multiplicative types.

def AddMonoidHom.toMultiplicative {α : Type u} {β : Type v} [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_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : Multiplicative α →* Multiplicative β) (a : α) : (toMultiplicative.symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

@[simp]

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

@[simp]

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

def MonoidHom.toAdditive {α : Type u} {β : Type v} [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_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : Additive α →+ Additive β) (a : α) : (toAdditive.symm f) a = Additive.toMul (f (Additive.ofMul a))

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

theorem AddMonoidHom.toMultiplicative'_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) (a : Additive α) : (toMultiplicative'.symm f) a = Multiplicative.toAdd (f (Additive.toMul a))

@[simp]

theorem AddMonoidHom.toMultiplicative'_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) (a : α) : (toMultiplicative' f) a = Multiplicative.ofAdd (f (Additive.ofMul a))

@[simp]

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

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

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

Equations

• MonoidHom.toAdditive' = AddMonoidHom.toMultiplicative'.symm

@[simp]

theorem MonoidHom.toAdditive'_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (a✝ : Additive α →+ β) (a : α) : (toAdditive'.symm a✝) a = Multiplicative.ofAdd (a✝ (Additive.ofMul a))

@[simp]

theorem MonoidHom.toAdditive'_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (a✝ : α →* Multiplicative β) (a : Additive α) : (toAdditive' a✝) a = Multiplicative.toAdd (a✝ (Additive.toMul a))

@[simp]

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

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

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

Equations

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

@[simp]

theorem AddMonoidHom.toMultiplicative''_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) (a : Multiplicative α) : (toMultiplicative'' f) a = Additive.toMul (f (Multiplicative.toAdd a))

@[simp]

theorem AddMonoidHom.toMultiplicative''_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) (a : α) : (toMultiplicative''.symm f) a = Additive.ofMul (f (Multiplicative.ofAdd a))

@[simp]

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

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

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

Equations

• MonoidHom.toAdditive'' = AddMonoidHom.toMultiplicative''.symm

@[simp]

theorem MonoidHom.toAdditive''_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (a✝ : α →+ Additive β) (a : Multiplicative α) : (toAdditive''.symm a✝) a = Additive.toMul (a✝ (Multiplicative.toAdd a))

@[simp]

theorem MonoidHom.toAdditive''_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (a✝ : Multiplicative α →* β) (a : α) : (toAdditive'' a✝) a = Additive.ofMul (a✝ (Multiplicative.ofAdd a))

@[simp]

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