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.

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
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 α) :
@[protected, instance]
def additive.inhabited {α : Type u} [inhabited α] :
Equations
@[protected, instance]
def additive.nontrivial {α : Type u} [nontrivial α] :
@[protected, instance]
@[protected, instance]
def additive.has_add {α : Type u} [has_mul α] :
Equations
@[simp]
@[simp]
theorem of_mul_mul {α : Type u} [has_mul α] (x y : α) :
@[simp]
theorem to_mul_add {α : Type u} [has_mul α] (x y : additive α) :
@[protected, instance]
def additive.add_semigroup {α : Type u} [semigroup α] :
Equations
@[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]
def multiplicative.has_one {α : Type u} [has_zero α] :
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]
def multiplicative.monoid {α : Type u} [h : add_monoid α] :
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 α) :
@[protected, instance]
def multiplicative.has_inv {α : Type u} [has_neg α] :
Equations
@[simp]
theorem of_add_neg {α : Type u} [has_neg α] (x : α) :
@[protected, instance]
def additive.has_sub {α : Type u} [has_div α] :
Equations
@[simp]
@[simp]
theorem of_mul_div {α : Type u} [has_div α] (x y : α) :
@[simp]
theorem to_mul_sub {α : Type u} [has_div α] (x y : additive α) :
def add_monoid_hom.to_multiplicative {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] :

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

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

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

Equations
@[simp]
theorem monoid_hom.to_additive_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] (f : α →* β) (a : additive α) :
def add_monoid_hom.to_multiplicative' {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] :

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

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

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

Equations
@[simp]
def add_monoid_hom.to_multiplicative'' {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] :

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

Equations
@[simp]
def monoid_hom.to_additive'' {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] :

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

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]
def multiplicative.has_coe_to_fun {α : Type u_1} {β : α → Sort u_2} [has_coe_to_fun α β] :

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