# mathlibdocumentation

algebra.group.type_tags

# Type tags that turn additive structures into multiplicative, and vice versa

We define two type tags:

• additive α: turns any multiplicative structure on α into the corresponding additive structure on additive α;
• multiplicative α: turns any additive structure on α into the corresponding multiplicative structure on multiplicative α.

We also define instances additive.* and multiplicative.* that actually transfer the structures.

Type u_1Type u_1

If α carries some multiplicative structure, then additive α carries the corresponding additive structure.

Equations
• = α
def multiplicative  :
Type u_1Type u_1

If α carries some additive structure, then multiplicative α carries the corresponding multiplicative structure.

Equations
def additive.of_mul {α : Type u} :
α

Reinterpret x : α as an element of additive α.

Equations
def additive.to_mul {α : Type u} :
α

Reinterpret x : additive α as an element of α.

Equations
@[simp]
theorem additive.of_mul_symm_eq {α : Type u} :

@[simp]
theorem additive.to_mul_symm_eq {α : Type u} :

def multiplicative.of_add {α : Type u} :

Reinterpret x : α as an element of multiplicative α.

Equations
def multiplicative.to_add {α : Type u} :

Reinterpret x : multiplicative α as an element of α.

Equations
@[simp]
theorem multiplicative.of_add_symm_eq {α : Type u} :

@[simp]
theorem multiplicative.to_add_symm_eq {α : Type u} :

@[simp]

@[simp]

@[simp]
theorem to_mul_of_mul {α : Type u} (x : α) :

@[simp]
theorem of_mul_to_mul {α : Type u} (x : additive α) :

@[instance]
def additive.inhabited {α : Type u} [inhabited α] :

Equations
@[instance]
def multiplicative.inhabited {α : Type u} [inhabited α] :

Equations
@[instance]

Equations
@[instance]
def multiplicative.has_mul {α : Type u} [has_add α] :

Equations
@[simp]

@[simp]
theorem to_add_mul {α : Type u} [has_add α] (x y : multiplicative α) :

@[simp]
theorem of_mul_mul {α : Type u} [has_mul α] (x y : α) :

@[simp]
theorem to_mul_add {α : Type u} [has_mul α] (x y : additive α) :

@[instance]

Equations
@[instance]
def multiplicative.semigroup {α : Type u}  :

Equations
@[instance]

Equations
@[instance]
def multiplicative.comm_semigroup {α : Type u}  :

Equations
@[instance]

Equations
@[instance]
def multiplicative.left_cancel_semigroup {α : Type u}  :

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def additive.has_zero {α : Type u} [has_one α] :

Equations
@[simp]
theorem of_mul_one {α : Type u} [has_one α] :

@[simp]
theorem to_mul_zero {α : Type u} [has_one α] :

@[instance]
def multiplicative.has_one {α : Type u} [has_zero α] :

Equations
@[simp]
theorem of_add_zero {α : Type u} [has_zero α] :

@[simp]
theorem to_add_one {α : Type u} [has_zero α] :

@[instance]

Equations
@[instance]
def multiplicative.monoid {α : Type u} [add_monoid α] :

Equations
@[instance]

Equations
@[instance]
def multiplicative.comm_monoid {α : Type u}  :

Equations
@[instance]
def additive.has_neg {α : Type u} [has_inv α] :

Equations
@[simp]
theorem of_mul_inv {α : Type u} [has_inv α] (x : α) :

@[simp]
theorem to_mul_neg {α : Type u} [has_inv α] (x : additive α) :

@[instance]
def multiplicative.has_inv {α : Type u} [has_neg α] :

Equations
@[simp]
theorem of_add_neg {α : Type u} [has_neg α] (x : α) :

@[simp]
theorem to_add_inv {α : Type u} [has_neg α] (x : multiplicative α) :

@[instance]

Equations
@[instance]
def multiplicative.group {α : Type u} [add_group α] :

Equations
@[instance]

Equations
@[instance]
def multiplicative.comm_group {α : Type u}  :

Equations
→+ β)

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

Equations
def monoid_hom.to_additive {α : Type u} {β : Type v} [monoid α] [monoid β] :

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

Equations
def add_monoid_hom.to_multiplicative' {α : Type u} {β : Type v} [monoid α] [add_monoid β] :

Reinterpret additive α →+ β as α →* multiplicative β.

Equations
def monoid_hom.to_additive' {α : Type u} {β : Type v} [monoid α] [add_monoid β] :

Reinterpret α →* multiplicative β as additive α →+ β.

Equations
def add_monoid_hom.to_multiplicative'' {α : Type u} {β : Type v} [add_monoid α] [monoid β] :
Reinterpret α →+ additive β as multiplicative α →* β.
Reinterpret multiplicative α →* β as α →+ additive β.