# mathlib3documentation

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:

• 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.

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
@[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]
@[simp]
@[simp]
@[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 multiplicative.inhabited {α : Type u} [inhabited α] :
Equations
@[protected, instance]
def additive.finite {α : Type u} [finite α] :
@[protected, instance]
def multiplicative.finite {α : Type u} [finite α] :
@[protected, instance]
def additive.infinite {α : Type u} [infinite α] :
@[protected, instance]
def multiplicative.infinite {α : Type u} [infinite α] :
@[protected, instance]
def additive.nontrivial {α : Type u} [nontrivial α] :
@[protected, instance]
@[protected, instance]
Equations
@[protected, 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 α) :
@[protected, instance]
Equations
@[protected, instance]
def multiplicative.semigroup {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def multiplicative.is_cancel_mul {α : Type u} [has_add α]  :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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} :
x = 1
@[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} :
x = 0
@[simp]
theorem to_add_one {α : Type u} [has_zero α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def multiplicative.monoid {α : Type u} [h : add_monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def multiplicative.comm_monoid {α : Type u}  :
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 : α) :
@[simp]
theorem to_add_inv {α : Type u} [has_neg α] (x : multiplicative α) :
@[protected, instance]
def additive.has_sub {α : Type u} [has_div α] :
Equations
@[protected, instance]
def multiplicative.has_div {α : Type u} [has_sub α] :
Equations
@[simp]
theorem of_add_sub {α : Type u} [has_sub α] (x y : α) :
@[simp]
theorem to_add_div {α : Type u} [has_sub α] (x y : multiplicative α) :
@[simp]
theorem of_mul_div {α : Type u} [has_div α] (x y : α) :
@[simp]
theorem to_mul_sub {α : Type u} [has_div α] (x y : additive α) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.sub_neg_monoid {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def multiplicative.group {α : Type u} [add_group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def multiplicative.comm_group {α : Type u}  :
Equations
def add_monoid_hom.to_multiplicative {α : Type u} {β : Type v}  :
→+ β)

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

Equations
@[simp]
theorem add_monoid_hom.to_multiplicative_symm_apply_apply {α : Type u} {β : Type v} (f : →* ) (a : α) :
@[simp]
theorem add_monoid_hom.to_multiplicative_apply_apply {α : Type u} {β : Type v} (f : α →+ β) (a : multiplicative α) :
def monoid_hom.to_additive {α : Type u} {β : Type v}  :

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

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

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

Equations
@[simp]
theorem monoid_hom.to_additive'_apply_apply {α : Type u} {β : Type v} (ᾰ : α →* ) (a : additive α) :
def monoid_hom.to_additive' {α : Type u} {β : Type v}  :

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

Equations
@[simp]
theorem monoid_hom.to_additive'_symm_apply_apply {α : Type u} {β : Type v} (ᾰ : →+ β) (a : α) :
a =
@[simp]
theorem add_monoid_hom.to_multiplicative''_symm_apply_apply {α : Type u} {β : Type v} (f : →* β) (a : α) :
@[simp]
theorem add_monoid_hom.to_multiplicative''_apply_apply {α : Type u} {β : Type v} (f : α →+ ) (a : multiplicative α) :
def add_monoid_hom.to_multiplicative'' {α : Type u} {β : Type v}  :

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

Equations
@[simp]
theorem monoid_hom.to_additive''_symm_apply_apply {α : Type u} {β : Type v} (ᾰ : α →+ ) (a : multiplicative α) :
a =
@[simp]
theorem monoid_hom.to_additive''_apply_apply {α : Type u} {β : Type v} (ᾰ : →* β) (a : α) :
def monoid_hom.to_additive'' {α : Type u} {β : Type v}  :

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

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

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} [ β] :
(λ (a : , β

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