mathlib documentation

algebra.group.type_tags

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

We define two type tags:

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

def additive  :
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
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 to_add_of_add {α : Type u} (x : α) :

@[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 additive.has_add {α : Type u} [has_mul α] :

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

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

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

@[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 α] :

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

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

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

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 α) :

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

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

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

Equations
def monoid_hom.to_additive {α : Type u} {β : Type v} [monoid α] [monoid β] :
→* β) (additive α →+ additive β)

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 α →* β.

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

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

Equations