mathlib3 documentation

algebra.group.type_tags

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define two type tags:

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

See also #

This file is similar to order.synonym.

def additive (α : Type u_1) :
Type u_1

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

Equations
Instances for additive
def multiplicative (α : Type u_1) :
Type u_1

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

Equations
Instances for multiplicative
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

Reinterpret x : α as an element of multiplicative α.

Equations

Reinterpret x : multiplicative α as an element of α.

Equations
@[simp]
@[simp]
theorem to_mul_of_mul {α : Type u} (x : α) :
@[simp]
theorem of_mul_to_mul {α : Type u} (x : additive α) :
@[protected, instance]
def additive.finite {α : Type u} [finite α] :
@[protected, instance]
@[protected, instance]
def additive.infinite {α : Type u} [infinite α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def additive.has_add {α : Type u} [has_mul α] :
Equations
@[simp]
theorem of_mul_mul {α : Type u} [has_mul α] (x y : α) :
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def additive.has_zero {α : Type u} [has_one α] :
Equations
@[simp]
theorem of_mul_one {α : Type u} [has_one α] :
@[simp]
theorem of_mul_eq_zero {A : Type u_1} [has_one A] {x : A} :
@[simp]
theorem to_mul_zero {α : Type u} [has_one α] :
@[protected, instance]
Equations
@[simp]
theorem of_add_zero {α : Type u} [has_zero α] :
@[simp]
theorem of_add_eq_one {A : Type u_1} [has_zero A] {x : A} :
@[simp]
theorem to_add_one {α : Type u} [has_zero α] :
@[protected, instance]
Equations
@[protected, instance]
def additive.add_monoid {α : Type u} [h : monoid α] :
Equations
@[protected, instance]
Equations
@[protected, 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]
@[protected, instance]
def additive.has_sub {α : Type u} [has_div α] :
Equations
@[simp]
theorem of_mul_div {α : Type u} [has_div α] (x y : α) :
@[simp]
def monoid_hom.to_additive {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] :
→* β) (additive α →+ additive β)

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

Equations

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

Equations

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

Equations
@[protected, instance]
def additive.has_coe_to_fun {α : Type u_1} {β : α Sort u_2} [has_coe_to_fun α β] :

If α has some multiplicative structure and coerces to a function, then additive α should also coerce to the same function.

This allows additive to be used on bundled function types with a multiplicative structure, which is often used for composition, without affecting the behavior of the function itself.

Equations
@[protected, instance]

If α has some additive structure and coerces to a function, then multiplicative α should also coerce to the same function.

This allows multiplicative to be used on bundled function types with an additive structure, which is often used for composition, without affecting the behavior of the function itself.

Equations