# Documentation

Mathlib.Algebra.Group.TypeTags

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

This file is similar to Order.Synonym.

## Porting notes #

• Since bundled morphism applications that rely on CoeFun currently don't work, they are ported as toFoo a rather than a.toFoo for now. (https://github.com/leanprover/lean4/issues/1910)
def Additive (α : Type u_1) :
Type u_1

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

Equations
• = α
Instances For
def Multiplicative (α : Type u_1) :
Type u_1

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

Equations
Instances For
def Additive.ofMul {α : Type u} :
α

Reinterpret x : α as an element of Additive α.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Additive.toMul {α : Type u} :
α

Reinterpret x : Additive α as an element of α.

Equations
Instances For
@[simp]
theorem Additive.ofMul_symm_eq {α : Type u} :
@[simp]
theorem Additive.toMul_symm_eq {α : Type u} :
def Multiplicative.ofAdd {α : Type u} :

Reinterpret x : α as an element of Multiplicative α.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Multiplicative.toAdd {α : Type u} :

Reinterpret x : Multiplicative α as an element of α.

Equations
Instances For
@[simp]
theorem Multiplicative.ofAdd_symm_eq {α : Type u} :
@[simp]
theorem Multiplicative.toAdd_symm_eq {α : Type u} :
@[simp]
@[simp]
@[simp]
theorem toMul_ofMul {α : Type u} (x : α) :
@[simp]
theorem ofMul_toMul {α : Type u} (x : ) :
instance instSubsingletonAdditive {α : Type u} [] :
Equations
• (_ : ) = (_ : )
instance instSubsingletonMultiplicative {α : Type u} [] :
Equations
• (_ : ) = (_ : )
instance instInhabitedAdditive {α : Type u} [] :
Equations
instance instInhabitedMultiplicative {α : Type u} [] :
Equations
• instInhabitedMultiplicative = { default := Multiplicative.ofAdd default }
instance instUniqueAdditive {α : Type u} [] :
Equations
instance instUniqueMultiplicative {α : Type u} [] :
Equations
instance instFiniteAdditive {α : Type u} [] :
Equations
instance instFiniteMultiplicative {α : Type u} [] :
Equations
• (_ : ) = (_ : )
instance instInfiniteAdditive {α : Type u} [h : ] :
Equations
instance instInfiniteMultiplicative {α : Type u} [h : ] :
Equations
• (_ : ) = h
instance instDecidableEqMultiplicative {α : Type u} [h : ] :
Equations
• instDecidableEqMultiplicative = h
instance instDecidableEqAdditive {α : Type u} [h : ] :
Equations
instance Additive.instNontrivial {α : Type u} [] :
Equations
• (_ : ) = (_ : )
instance Multiplicative.instNontrivial {α : Type u} [] :
Equations
• (_ : ) = (_ : )
Equations
instance Multiplicative.mul {α : Type u} [Add α] :
Equations
• Multiplicative.mul = { mul := fun (x y : ) => Multiplicative.ofAdd (Multiplicative.toAdd x + Multiplicative.toAdd y) }
@[simp]
@[simp]
theorem toAdd_mul {α : Type u} [Add α] (x : ) (y : ) :
@[simp]
theorem ofMul_mul {α : Type u} [Mul α] (x : α) (y : α) :
@[simp]
theorem toMul_add {α : Type u} [Mul α] (x : ) (y : ) :
Equations
instance Multiplicative.semigroup {α : Type u} [] :
Equations
• Multiplicative.semigroup = let src := Multiplicative.mul; Semigroup.mk (_ : ∀ (a b c : α), a + b + c = a + (b + c))
Equations
instance Multiplicative.commSemigroup {α : Type u} [] :
Equations
• Multiplicative.commSemigroup = let src := Multiplicative.semigroup; CommSemigroup.mk (_ : ∀ (a b : α), a + b = b + a)
Equations
• (_ : ) = (_ : )
instance Multiplicative.isLeftCancelMul {α : Type u} [Add α] [] :
Equations
• (_ : ) = (_ : )
Equations
• (_ : ) = (_ : )
instance Multiplicative.isRightCancelMul {α : Type u} [Add α] [] :
Equations
• (_ : ) = (_ : )
Equations
• (_ : ) = (_ : )
instance Multiplicative.isCancelMul {α : Type u} [Add α] [] :
Equations
• (_ : ) = (_ : )
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance instZeroAdditive {α : Type u} [One α] :
Zero ()
Equations
@[simp]
theorem ofMul_one {α : Type u} [One α] :
@[simp]
theorem ofMul_eq_zero {A : Type u_1} [One A] {x : A} :
Additive.ofMul x = 0 x = 1
@[simp]
theorem toMul_zero {α : Type u} [One α] :
instance instOneMultiplicative {α : Type u} [Zero α] :
Equations
• instOneMultiplicative = { one := Multiplicative.ofAdd 0 }
@[simp]
theorem ofAdd_zero {α : Type u} [Zero α] :
@[simp]
theorem ofAdd_eq_one {A : Type u_1} [Zero A] {x : A} :
Multiplicative.ofAdd x = 1 x = 0
@[simp]
theorem toAdd_one {α : Type u} [Zero α] :
Equations
instance Multiplicative.mulOneClass {α : Type u} [] :
Equations
• Multiplicative.mulOneClass = MulOneClass.mk (_ : ∀ (a : α), 0 + a = a) (_ : ∀ (a : α), a + 0 = a)
Equations
instance Multiplicative.monoid {α : Type u} [h : ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ofMul_pow {α : Type u} [] (n : ) (a : α) :
@[simp]
theorem toMul_nsmul {α : Type u} [] (n : ) (a : ) :
@[simp]
theorem ofAdd_nsmul {α : Type u} [] (n : ) (a : α) :
@[simp]
theorem toAdd_pow {α : Type u} [] (a : ) (n : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
instance Multiplicative.commMonoid {α : Type u} [] :
Equations
• Multiplicative.commMonoid = let src := Multiplicative.monoid; let src_1 := Multiplicative.commSemigroup; CommMonoid.mk (_ : ∀ (a b : ), a * b = b * a)
instance Additive.neg {α : Type u} [Inv α] :
Neg ()
Equations
@[simp]
theorem ofMul_inv {α : Type u} [Inv α] (x : α) :
@[simp]
theorem toMul_neg {α : Type u} [Inv α] (x : ) :
instance Multiplicative.inv {α : Type u} [Neg α] :
Equations
• Multiplicative.inv = { inv := fun (x : ) => Additive.ofMul (-Multiplicative.toAdd x) }
@[simp]
theorem ofAdd_neg {α : Type u} [Neg α] (x : α) :
@[simp]
theorem toAdd_inv {α : Type u} [Neg α] (x : ) :
instance Additive.sub {α : Type u} [Div α] :
Sub ()
Equations
instance Multiplicative.div {α : Type u} [Sub α] :
Equations
• Multiplicative.div = { div := fun (x y : ) => Multiplicative.ofAdd (Multiplicative.toAdd x - Multiplicative.toAdd y) }
@[simp]
theorem ofAdd_sub {α : Type u} [Sub α] (x : α) (y : α) :
@[simp]
theorem toAdd_div {α : Type u} [Sub α] (x : ) (y : ) :
@[simp]
theorem ofMul_div {α : Type u} [Div α] (x : α) (y : α) :
@[simp]
theorem toMul_sub {α : Type u} [Div α] (x : ) (y : ) :
instance Additive.involutiveNeg {α : Type u} [] :
Equations
instance Multiplicative.involutiveInv {α : Type u} [] :
Equations
• Multiplicative.involutiveInv = let src := Multiplicative.inv; InvolutiveInv.mk (_ : ∀ (a : α), - -a = a)
instance Additive.subNegMonoid {α : Type u} [] :
Equations
instance Multiplicative.divInvMonoid {α : Type u} [] :
Equations
• Multiplicative.divInvMonoid = let src := Multiplicative.inv; let src_1 := Multiplicative.div; let src_2 := Multiplicative.monoid; DivInvMonoid.mk SubNegMonoid.zsmul
@[simp]
theorem ofMul_zpow {α : Type u} [] (z : ) (a : α) :
@[simp]
theorem toMul_zsmul {α : Type u} [] (z : ) (a : ) :
@[simp]
theorem ofAdd_zsmul {α : Type u} [] (z : ) (a : α) :
@[simp]
theorem toAdd_zpow {α : Type u} [] (a : ) (z : ) :
instance Additive.subtractionMonoid {α : Type u} [] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• Additive.subtractionCommMonoid = let src := Additive.subtractionMonoid; let src_1 := Additive.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : ), a + b = b + a)
Equations
• Multiplicative.divisionCommMonoid = let src := Multiplicative.divisionMonoid; let src_1 := Multiplicative.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : ), a * b = b * a)
Equations
instance Multiplicative.group {α : Type u} [] :
Equations
• Multiplicative.group = let src := Multiplicative.divInvMonoid; Group.mk (_ : ∀ (a : α), -a + a = 0)
Equations
instance Multiplicative.commGroup {α : Type u} [] :
Equations
• Multiplicative.commGroup = let src := Multiplicative.group; let src_1 := Multiplicative.commMonoid; CommGroup.mk (_ : ∀ (a b : ), a * b = b * a)
@[simp]
theorem AddMonoidHom.toMultiplicative_apply_apply {α : Type u} {β : Type v} [] [] (f : α →+ β) (a : ) :
@[simp]
theorem AddMonoidHom.toMultiplicative_symm_apply_apply {α : Type u} {β : Type v} [] [] (f : ) (a : α) :
def AddMonoidHom.toMultiplicative {α : Type u} {β : Type v} [] [] :
(α →+ β) ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MonoidHom.toAdditive_apply_apply {α : Type u} {β : Type v} [] [] (f : α →* β) (a : ) :
@[simp]
theorem MonoidHom.toAdditive_symm_apply_apply {α : Type u} {β : Type v} [] [] (f : ) (a : α) :
def MonoidHom.toAdditive {α : Type u} {β : Type v} [] [] :
(α →* β) ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddMonoidHom.toMultiplicative'_apply_apply {α : Type u} {β : Type v} [] [] (f : →+ β) (a : α) :
@[simp]
theorem AddMonoidHom.toMultiplicative'_symm_apply_apply {α : Type u} {β : Type v} [] [] (f : ) (a : ) :
def AddMonoidHom.toMultiplicative' {α : Type u} {β : Type v} [] [] :
( →+ β) ()

Reinterpret Additive α →+ β as α →* Multiplicative β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MonoidHom.toAdditive'_apply_apply {α : Type u} {β : Type v} [] [] :
@[simp]
theorem MonoidHom.toAdditive'_symm_apply_apply {α : Type u} {β : Type v} [] [] :
def MonoidHom.toAdditive' {α : Type u} {β : Type v} [] [] :
() ( →+ β)

Reinterpret α →* Multiplicative β as Additive α →+ β.

Equations
Instances For
@[simp]
theorem AddMonoidHom.toMultiplicative''_symm_apply_apply {α : Type u} {β : Type v} [] [] (f : ) (a : α) :
@[simp]
theorem AddMonoidHom.toMultiplicative''_apply_apply {α : Type u} {β : Type v} [] [] (f : α →+ ) (a : ) :
def AddMonoidHom.toMultiplicative'' {α : Type u} {β : Type v} [] [] :
(α →+ ) ()

Reinterpret α →+ Additive β as Multiplicative α →* β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MonoidHom.toAdditive''_symm_apply_apply {α : Type u} {β : Type v} [] [] :
∀ (a : α →+ ) (a_1 : ), (MonoidHom.toAdditive''.symm a) a_1 = Additive.toMul (a (Multiplicative.toAdd a_1))
@[simp]
theorem MonoidHom.toAdditive''_apply_apply {α : Type u} {β : Type v} [] [] :
def MonoidHom.toAdditive'' {α : Type u} {β : Type v} [] [] :
() (α →+ )

Reinterpret Multiplicative α →* β as α →+ Additive β.

Equations
Instances For
instance Additive.coeToFun {α : Type u_1} {β : αSort u_2} [CoeFun α β] :
CoeFun () fun (a : ) => β (Additive.toMul a)

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
• Additive.coeToFun = { coe := fun (a : ) => CoeFun.coe (Additive.toMul a) }
instance Multiplicative.coeToFun {α : Type u_1} {β : αSort u_2} [CoeFun α β] :
CoeFun () fun (a : ) => β (Multiplicative.toAdd 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
• Multiplicative.coeToFun = { coe := fun (a : ) => CoeFun.coe (Multiplicative.toAdd a) }